proof (prove): step 18

using this:
  ideal (carrier (Z2∷int set ring)) Z2
  (h∷int set ⇒ int set × int set) ∈ ring_hom (Z2∷int set ring) (Z2Z2∷(int set × int set) ring)
  ¬ ideal ((h∷int set ⇒ int set × int set) ` carrier (Z2∷int set ring)) (Z2Z2∷(int set × int set) ring)
  ideal (?I∷'a set) (?R∷('a, 'b) ring_scheme) ⟹
  (?h∷'a ⇒ 'c) ∈ ring_hom ?R (?S∷('c, 'd) ring_scheme) ⟹ ¬ ideal (?h ` ?I) ?S ⟹ thesis∷bool

goal (1 subgoal):
 1. thesis
variables:
  thesis :: bool