zf_lang1.miz



    begin

    reserve p,p1,p2,q,r,F,G,G1,G2,H,H1,H2 for ZF-formula,

x,x1,x2,y,y1,y2,z,z1,z2,s,t for Variable,

a,X for set;

    theorem :: ZF_LANG1:1

    

     Th1: ( Var1 (x '=' y)) = x & ( Var2 (x '=' y)) = y

    proof

      (x '=' y) is being_equality;

      then (x '=' y) = (( Var1 (x '=' y)) '=' ( Var2 (x '=' y))) by ZF_LANG: 36;

      hence thesis by ZF_LANG: 1;

    end;

    theorem :: ZF_LANG1:2

    

     Th2: ( Var1 (x 'in' y)) = x & ( Var2 (x 'in' y)) = y

    proof

      (x 'in' y) is being_membership;

      then (x 'in' y) = (( Var1 (x 'in' y)) 'in' ( Var2 (x 'in' y))) by ZF_LANG: 37;

      hence thesis by ZF_LANG: 2;

    end;

    theorem :: ZF_LANG1:3

    

     Th3: ( the_argument_of ( 'not' p)) = p

    proof

      ( 'not' p) is negative;

      hence thesis by ZF_LANG:def 30;

    end;

    theorem :: ZF_LANG1:4

    

     Th4: ( the_left_argument_of (p '&' q)) = p & ( the_right_argument_of (p '&' q)) = q

    proof

      (p '&' q) is conjunctive;

      then (p '&' q) = (( the_left_argument_of (p '&' q)) '&' ( the_right_argument_of (p '&' q))) by ZF_LANG: 40;

      hence thesis by ZF_LANG: 30;

    end;

    theorem :: ZF_LANG1:5

    ( the_left_argument_of (p 'or' q)) = p & ( the_right_argument_of (p 'or' q)) = q

    proof

      (p 'or' q) is disjunctive;

      then (p 'or' q) = (( the_left_argument_of (p 'or' q)) 'or' ( the_right_argument_of (p 'or' q))) by ZF_LANG: 41;

      hence thesis by ZF_LANG: 31;

    end;

    theorem :: ZF_LANG1:6

    

     Th6: ( the_antecedent_of (p => q)) = p & ( the_consequent_of (p => q)) = q

    proof

      (p => q) is conditional;

      then (p => q) = (( the_antecedent_of (p => q)) => ( the_consequent_of (p => q))) by ZF_LANG: 47;

      hence thesis by ZF_LANG: 32;

    end;

    theorem :: ZF_LANG1:7

    ( the_left_side_of (p <=> q)) = p & ( the_right_side_of (p <=> q)) = q

    proof

      (p <=> q) is biconditional;

      then (p <=> q) = (( the_left_side_of (p <=> q)) <=> ( the_right_side_of (p <=> q))) by ZF_LANG: 49;

      hence thesis by ZF_LANG: 33;

    end;

    theorem :: ZF_LANG1:8

    

     Th8: ( bound_in ( All (x,p))) = x & ( the_scope_of ( All (x,p))) = p

    proof

      ( All (x,p)) is universal;

      then ( All (x,p)) = ( All (( bound_in ( All (x,p))),( the_scope_of ( All (x,p))))) by ZF_LANG: 44;

      hence thesis by ZF_LANG: 3;

    end;

    theorem :: ZF_LANG1:9

    

     Th9: ( bound_in ( Ex (x,p))) = x & ( the_scope_of ( Ex (x,p))) = p

    proof

      ( Ex (x,p)) is existential;

      then ( Ex (x,p)) = ( Ex (( bound_in ( Ex (x,p))),( the_scope_of ( Ex (x,p))))) by ZF_LANG: 45;

      hence thesis by ZF_LANG: 34;

    end;

    theorem :: ZF_LANG1:10

    (p 'or' q) = (( 'not' p) => q);

    theorem :: ZF_LANG1:11

    ( All (x,y,p)) is universal & ( bound_in ( All (x,y,p))) = x & ( the_scope_of ( All (x,y,p))) = ( All (y,p)) by Th8;

    theorem :: ZF_LANG1:12

    ( Ex (x,y,p)) is existential & ( bound_in ( Ex (x,y,p))) = x & ( the_scope_of ( Ex (x,y,p))) = ( Ex (y,p)) by Th9;

    theorem :: ZF_LANG1:13

    ( All (x,y,z,p)) = ( All (x,( All (y,( All (z,p)))))) & ( All (x,y,z,p)) = ( All (x,y,( All (z,p))));

    theorem :: ZF_LANG1:14

    

     Th14: ( All (x1,y1,p1)) = ( All (x2,y2,p2)) implies x1 = x2 & y1 = y2 & p1 = p2

    proof

      assume

       A1: ( All (x1,y1,p1)) = ( All (x2,y2,p2));

      then ( All (y1,p1)) = ( All (y2,p2)) by ZF_LANG: 3;

      hence thesis by A1, ZF_LANG: 3;

    end;

    theorem :: ZF_LANG1:15

    ( All (x1,y1,z1,p1)) = ( All (x2,y2,z2,p2)) implies x1 = x2 & y1 = y2 & z1 = z2 & p1 = p2

    proof

      assume

       A1: ( All (x1,y1,z1,p1)) = ( All (x2,y2,z2,p2));

      then ( All (y1,z1,p1)) = ( All (y2,z2,p2)) by ZF_LANG: 3;

      hence thesis by A1, Th14, ZF_LANG: 3;

    end;

    theorem :: ZF_LANG1:16

    ( All (x,y,z,p)) = ( All (t,s,q)) implies x = t & y = s & ( All (z,p)) = q

    proof

      ( All (x,y,z,p)) = ( All (x,y,( All (z,p))));

      hence thesis by Th14;

    end;

    theorem :: ZF_LANG1:17

    

     Th17: ( Ex (x1,y1,p1)) = ( Ex (x2,y2,p2)) implies x1 = x2 & y1 = y2 & p1 = p2

    proof

      assume

       A1: ( Ex (x1,y1,p1)) = ( Ex (x2,y2,p2));

      then ( Ex (y1,p1)) = ( Ex (y2,p2)) by ZF_LANG: 34;

      hence thesis by A1, ZF_LANG: 34;

    end;

    theorem :: ZF_LANG1:18

    ( Ex (x,y,z,p)) = ( Ex (x,( Ex (y,( Ex (z,p)))))) & ( Ex (x,y,z,p)) = ( Ex (x,y,( Ex (z,p))));

    theorem :: ZF_LANG1:19

    ( Ex (x1,y1,z1,p1)) = ( Ex (x2,y2,z2,p2)) implies x1 = x2 & y1 = y2 & z1 = z2 & p1 = p2

    proof

      assume

       A1: ( Ex (x1,y1,z1,p1)) = ( Ex (x2,y2,z2,p2));

      then ( Ex (y1,z1,p1)) = ( Ex (y2,z2,p2)) by ZF_LANG: 34;

      hence thesis by A1, Th17, ZF_LANG: 34;

    end;

    theorem :: ZF_LANG1:20

    ( Ex (x,y,z,p)) = ( Ex (t,s,q)) implies x = t & y = s & ( Ex (z,p)) = q

    proof

      ( Ex (x,y,z,p)) = ( Ex (x,y,( Ex (z,p))));

      hence thesis by Th17;

    end;

    theorem :: ZF_LANG1:21

    ( All (x,y,z,p)) is universal & ( bound_in ( All (x,y,z,p))) = x & ( the_scope_of ( All (x,y,z,p))) = ( All (y,z,p)) by Th8;

    theorem :: ZF_LANG1:22

    ( Ex (x,y,z,p)) is existential & ( bound_in ( Ex (x,y,z,p))) = x & ( the_scope_of ( Ex (x,y,z,p))) = ( Ex (y,z,p)) by Th9;

    theorem :: ZF_LANG1:23

    H is disjunctive implies ( the_left_argument_of H) = ( the_argument_of ( the_left_argument_of ( the_argument_of H)))

    proof

      assume H is disjunctive;

      then H = (( the_left_argument_of H) 'or' ( the_right_argument_of H)) by ZF_LANG: 41;

      then ( the_argument_of H) = (( 'not' ( the_left_argument_of H)) '&' ( 'not' ( the_right_argument_of H))) by Th3;

      then ( the_left_argument_of ( the_argument_of H)) = ( 'not' ( the_left_argument_of H)) by Th4;

      hence thesis by Th3;

    end;

    theorem :: ZF_LANG1:24

    H is disjunctive implies ( the_right_argument_of H) = ( the_argument_of ( the_right_argument_of ( the_argument_of H)))

    proof

      assume H is disjunctive;

      then H = (( the_left_argument_of H) 'or' ( the_right_argument_of H)) by ZF_LANG: 41;

      then ( the_argument_of H) = (( 'not' ( the_left_argument_of H)) '&' ( 'not' ( the_right_argument_of H))) by Th3;

      then ( the_right_argument_of ( the_argument_of H)) = ( 'not' ( the_right_argument_of H)) by Th4;

      hence thesis by Th3;

    end;

    theorem :: ZF_LANG1:25

    H is conditional implies ( the_antecedent_of H) = ( the_left_argument_of ( the_argument_of H))

    proof

      assume H is conditional;

      then H = (( the_antecedent_of H) => ( the_consequent_of H)) by ZF_LANG: 47;

      then ( the_argument_of H) = (( the_antecedent_of H) '&' ( 'not' ( the_consequent_of H))) by Th3;

      hence thesis by Th4;

    end;

    theorem :: ZF_LANG1:26

    H is conditional implies ( the_consequent_of H) = ( the_argument_of ( the_right_argument_of ( the_argument_of H)))

    proof

      assume H is conditional;

      then H = (( the_antecedent_of H) => ( the_consequent_of H)) by ZF_LANG: 47;

      then ( the_argument_of H) = (( the_antecedent_of H) '&' ( 'not' ( the_consequent_of H))) by Th3;

      then ( the_right_argument_of ( the_argument_of H)) = ( 'not' ( the_consequent_of H)) by Th4;

      hence thesis by Th3;

    end;

    theorem :: ZF_LANG1:27

    H is biconditional implies ( the_left_side_of H) = ( the_antecedent_of ( the_left_argument_of H)) & ( the_left_side_of H) = ( the_consequent_of ( the_right_argument_of H))

    proof

      assume H is biconditional;

      then H = (( the_left_side_of H) <=> ( the_right_side_of H)) by ZF_LANG: 49;

      then ( the_left_argument_of H) = (( the_left_side_of H) => ( the_right_side_of H)) & ( the_right_argument_of H) = (( the_right_side_of H) => ( the_left_side_of H)) by Th4;

      hence thesis by Th6;

    end;

    theorem :: ZF_LANG1:28

    H is biconditional implies ( the_right_side_of H) = ( the_consequent_of ( the_left_argument_of H)) & ( the_right_side_of H) = ( the_antecedent_of ( the_right_argument_of H))

    proof

      assume H is biconditional;

      then H = (( the_left_side_of H) <=> ( the_right_side_of H)) by ZF_LANG: 49;

      then ( the_left_argument_of H) = (( the_left_side_of H) => ( the_right_side_of H)) & ( the_right_argument_of H) = (( the_right_side_of H) => ( the_left_side_of H)) by Th4;

      hence thesis by Th6;

    end;

    theorem :: ZF_LANG1:29

    H is existential implies ( bound_in H) = ( bound_in ( the_argument_of H)) & ( the_scope_of H) = ( the_argument_of ( the_scope_of ( the_argument_of H)))

    proof

      assume H is existential;

      then H = ( Ex (( bound_in H),( the_scope_of H))) by ZF_LANG: 45;

      then

       A1: ( the_argument_of H) = ( All (( bound_in H),( 'not' ( the_scope_of H)))) by Th3;

      hence ( bound_in H) = ( bound_in ( the_argument_of H)) by Th8;

      ( 'not' ( the_scope_of H)) = ( the_scope_of ( the_argument_of H)) by A1, Th8;

      hence thesis by Th3;

    end;

    theorem :: ZF_LANG1:30

    ( the_argument_of (F 'or' G)) = (( 'not' F) '&' ( 'not' G)) & ( the_antecedent_of (F 'or' G)) = ( 'not' F) & ( the_consequent_of (F 'or' G)) = G

    proof

      thus ( the_argument_of (F 'or' G)) = (( 'not' F) '&' ( 'not' G)) by Th3;

      (F 'or' G) = (( 'not' F) => G);

      hence thesis by Th6;

    end;

    theorem :: ZF_LANG1:31

    ( the_argument_of (F => G)) = (F '&' ( 'not' G)) by Th3;

    theorem :: ZF_LANG1:32

    ( the_left_argument_of (F <=> G)) = (F => G) & ( the_right_argument_of (F <=> G)) = (G => F) by Th4;

    theorem :: ZF_LANG1:33

    ( the_argument_of ( Ex (x,H))) = ( All (x,( 'not' H))) by Th3;

    theorem :: ZF_LANG1:34

    H is disjunctive implies H is conditional & H is negative & ( the_argument_of H) is conjunctive & ( the_left_argument_of ( the_argument_of H)) is negative & ( the_right_argument_of ( the_argument_of H)) is negative

    proof

      assume H is disjunctive;

      then

       A1: H = (( the_left_argument_of H) 'or' ( the_right_argument_of H)) by ZF_LANG: 41;

      then H = (( 'not' ( the_left_argument_of H)) => ( the_right_argument_of H));

      hence H is conditional & H is negative;

      

       A2: ( the_argument_of H) = (( 'not' ( the_left_argument_of H)) '&' ( 'not' ( the_right_argument_of H))) by A1, Th3;

      hence ( the_argument_of H) is conjunctive;

      ( the_left_argument_of ( the_argument_of H)) = ( 'not' ( the_left_argument_of H)) & ( the_right_argument_of ( the_argument_of H)) = ( 'not' ( the_right_argument_of H)) by A2, Th4;

      hence thesis;

    end;

    theorem :: ZF_LANG1:35

    H is conditional implies H is negative & ( the_argument_of H) is conjunctive & ( the_right_argument_of ( the_argument_of H)) is negative

    proof

      assume H is conditional;

      then

       A1: H = (( the_antecedent_of H) => ( the_consequent_of H)) by ZF_LANG: 47;

      hence H is negative;

      

       A2: ( the_argument_of H) = (( the_antecedent_of H) '&' ( 'not' ( the_consequent_of H))) by A1, Th3;

      hence ( the_argument_of H) is conjunctive;

      ( the_right_argument_of ( the_argument_of H)) = ( 'not' ( the_consequent_of H)) by A2, Th4;

      hence thesis;

    end;

    theorem :: ZF_LANG1:36

    H is biconditional implies H is conjunctive & ( the_left_argument_of H) is conditional & ( the_right_argument_of H) is conditional by Th4;

    theorem :: ZF_LANG1:37

    H is existential implies H is negative & ( the_argument_of H) is universal & ( the_scope_of ( the_argument_of H)) is negative

    proof

      assume H is existential;

      then

       A1: H = ( Ex (( bound_in H),( the_scope_of H))) by ZF_LANG: 45;

      hence H is negative;

      

       A2: ( the_argument_of H) = ( All (( bound_in H),( 'not' ( the_scope_of H)))) by A1, Th3;

      hence ( the_argument_of H) is universal;

      ( 'not' ( the_scope_of H)) = ( the_scope_of ( the_argument_of H)) by A2, Th8;

      hence thesis;

    end;

    theorem :: ZF_LANG1:38

     not (H is being_equality & (H is being_membership or H is negative or H is conjunctive or H is universal)) & not (H is being_membership & (H is negative or H is conjunctive or H is universal)) & not (H is negative & (H is conjunctive or H is universal)) & not (H is conjunctive & H is universal)

    proof

      (H . 1) = 0 or (H . 1) = 1 or (H . 1) = 2 or (H . 1) = 3 or (H . 1) = 4 by ZF_LANG: 23;

      hence thesis by ZF_LANG: 18, ZF_LANG: 19, ZF_LANG: 20, ZF_LANG: 21, ZF_LANG: 22;

    end;

    theorem :: ZF_LANG1:39

    

     Th39: F is_subformula_of G implies ( len F) <= ( len G) by ZF_LANG:def 41, ZF_LANG: 62;

    theorem :: ZF_LANG1:40

    

     Th40: F is_proper_subformula_of G & G is_subformula_of H or F is_subformula_of G & G is_proper_subformula_of H or F is_subformula_of G & G is_immediate_constituent_of H or F is_immediate_constituent_of G & G is_subformula_of H or F is_proper_subformula_of G & G is_immediate_constituent_of H or F is_immediate_constituent_of G & G is_proper_subformula_of H implies F is_proper_subformula_of H

    proof

      

       A1: F is_immediate_constituent_of G implies F is_proper_subformula_of G by ZF_LANG: 61;

       A2:

      now

        assume

         A3: F is_proper_subformula_of G;

        then

         A4: ( len F) < ( len G) by ZF_LANG: 62;

        assume

         A5: G is_subformula_of H;

        F is_subformula_of G by A3;

        then

         A6: F is_subformula_of H by A5, ZF_LANG: 65;

        ( len G) <= ( len H) by A5, Th39;

        hence F is_proper_subformula_of H by A4, A6;

      end;

      G is_immediate_constituent_of H implies G is_proper_subformula_of H by ZF_LANG: 61;

      hence thesis by A2, A1;

    end;

    theorem :: ZF_LANG1:41

     not H is_immediate_constituent_of H

    proof

      assume H is_immediate_constituent_of H;

      then H is_proper_subformula_of H by ZF_LANG: 61;

      hence contradiction;

    end;

    theorem :: ZF_LANG1:42

     not (G is_proper_subformula_of H & H is_subformula_of G)

    proof

      assume G is_proper_subformula_of H & H is_subformula_of G;

      then G is_proper_subformula_of G by Th40;

      hence contradiction;

    end;

    theorem :: ZF_LANG1:43

     not (G is_proper_subformula_of H & H is_proper_subformula_of G)

    proof

      assume G is_proper_subformula_of H & H is_proper_subformula_of G;

      then G is_proper_subformula_of G by ZF_LANG: 64;

      hence contradiction;

    end;

    theorem :: ZF_LANG1:44

     not (G is_subformula_of H & H is_immediate_constituent_of G)

    proof

      assume G is_subformula_of H & H is_immediate_constituent_of G;

      then G is_proper_subformula_of G by Th40;

      hence contradiction;

    end;

    theorem :: ZF_LANG1:45

     not (G is_proper_subformula_of H & H is_immediate_constituent_of G)

    proof

      assume G is_proper_subformula_of H & H is_immediate_constituent_of G;

      then G is_proper_subformula_of G by Th40;

      hence contradiction;

    end;

    theorem :: ZF_LANG1:46

    ( 'not' F) is_subformula_of H implies F is_proper_subformula_of H

    proof

      F is_immediate_constituent_of ( 'not' F);

      hence thesis by Th40;

    end;

    theorem :: ZF_LANG1:47

    (F '&' G) is_subformula_of H implies F is_proper_subformula_of H & G is_proper_subformula_of H

    proof

      F is_immediate_constituent_of (F '&' G) & G is_immediate_constituent_of (F '&' G);

      hence thesis by Th40;

    end;

    theorem :: ZF_LANG1:48

    ( All (x,H)) is_subformula_of F implies H is_proper_subformula_of F

    proof

      H is_immediate_constituent_of ( All (x,H));

      hence thesis by Th40;

    end;

    theorem :: ZF_LANG1:49

    (F '&' ( 'not' G)) is_proper_subformula_of (F => G) & F is_proper_subformula_of (F => G) & ( 'not' G) is_proper_subformula_of (F => G) & G is_proper_subformula_of (F => G)

    proof

      (F '&' ( 'not' G)) is_immediate_constituent_of (F => G);

      hence

       A1: (F '&' ( 'not' G)) is_proper_subformula_of (F => G) by ZF_LANG: 61;

      F is_immediate_constituent_of (F '&' ( 'not' G)) & ( 'not' G) is_immediate_constituent_of (F '&' ( 'not' G));

      hence

       A2: F is_proper_subformula_of (F => G) & ( 'not' G) is_proper_subformula_of (F => G) by A1, Th40;

      G is_immediate_constituent_of ( 'not' G);

      hence thesis by A2, Th40;

    end;

    theorem :: ZF_LANG1:50

    (( 'not' F) '&' ( 'not' G)) is_proper_subformula_of (F 'or' G) & ( 'not' F) is_proper_subformula_of (F 'or' G) & ( 'not' G) is_proper_subformula_of (F 'or' G) & F is_proper_subformula_of (F 'or' G) & G is_proper_subformula_of (F 'or' G)

    proof

      (( 'not' F) '&' ( 'not' G)) is_immediate_constituent_of (F 'or' G);

      hence

       A1: (( 'not' F) '&' ( 'not' G)) is_proper_subformula_of (F 'or' G) by ZF_LANG: 61;

      ( 'not' F) is_immediate_constituent_of (( 'not' F) '&' ( 'not' G)) & ( 'not' G) is_immediate_constituent_of (( 'not' F) '&' ( 'not' G));

      hence

       A2: ( 'not' F) is_proper_subformula_of (F 'or' G) & ( 'not' G) is_proper_subformula_of (F 'or' G) by A1, Th40;

      F is_immediate_constituent_of ( 'not' F) & G is_immediate_constituent_of ( 'not' G);

      hence thesis by A2, Th40;

    end;

    theorem :: ZF_LANG1:51

    ( All (x,( 'not' H))) is_proper_subformula_of ( Ex (x,H)) & ( 'not' H) is_proper_subformula_of ( Ex (x,H))

    proof

      ( All (x,( 'not' H))) is_immediate_constituent_of ( Ex (x,H));

      hence

       A1: ( All (x,( 'not' H))) is_proper_subformula_of ( Ex (x,H)) by ZF_LANG: 61;

      ( 'not' H) is_immediate_constituent_of ( All (x,( 'not' H)));

      hence thesis by A1, Th40;

    end;

    theorem :: ZF_LANG1:52

    G is_subformula_of H iff G in ( Subformulae H) by ZF_LANG: 78, ZF_LANG:def 42;

    theorem :: ZF_LANG1:53

    G in ( Subformulae H) implies ( Subformulae G) c= ( Subformulae H) by ZF_LANG: 78, ZF_LANG: 79;

    theorem :: ZF_LANG1:54

    H in ( Subformulae H)

    proof

      H is_subformula_of H by ZF_LANG: 59;

      hence thesis by ZF_LANG:def 42;

    end;

    theorem :: ZF_LANG1:55

    

     Th55: ( Subformulae (F => G)) = ((( Subformulae F) \/ ( Subformulae G)) \/ {( 'not' G), (F '&' ( 'not' G)), (F => G)})

    proof

      

      thus ( Subformulae (F => G)) = (( Subformulae (F '&' ( 'not' G))) \/ {(F => G)}) by ZF_LANG: 82

      .= (((( Subformulae F) \/ ( Subformulae ( 'not' G))) \/ {(F '&' ( 'not' G))}) \/ {(F => G)}) by ZF_LANG: 83

      .= (((( Subformulae F) \/ (( Subformulae G) \/ {( 'not' G)})) \/ {(F '&' ( 'not' G))}) \/ {(F => G)}) by ZF_LANG: 82

      .= ((((( Subformulae F) \/ ( Subformulae G)) \/ {( 'not' G)}) \/ {(F '&' ( 'not' G))}) \/ {(F => G)}) by XBOOLE_1: 4

      .= (((( Subformulae F) \/ ( Subformulae G)) \/ {( 'not' G)}) \/ ( {(F '&' ( 'not' G))} \/ {(F => G)})) by XBOOLE_1: 4

      .= ((( Subformulae F) \/ ( Subformulae G)) \/ ( {( 'not' G)} \/ ( {(F '&' ( 'not' G))} \/ {(F => G)}))) by XBOOLE_1: 4

      .= ((( Subformulae F) \/ ( Subformulae G)) \/ ( {( 'not' G)} \/ {(F '&' ( 'not' G)), (F => G)})) by ENUMSET1: 1

      .= ((( Subformulae F) \/ ( Subformulae G)) \/ {( 'not' G), (F '&' ( 'not' G)), (F => G)}) by ENUMSET1: 2;

    end;

    theorem :: ZF_LANG1:56

    ( Subformulae (F 'or' G)) = ((( Subformulae F) \/ ( Subformulae G)) \/ {( 'not' G), ( 'not' F), (( 'not' F) '&' ( 'not' G)), (F 'or' G)})

    proof

      

      thus ( Subformulae (F 'or' G)) = (( Subformulae (( 'not' F) '&' ( 'not' G))) \/ {(F 'or' G)}) by ZF_LANG: 82

      .= (((( Subformulae ( 'not' F)) \/ ( Subformulae ( 'not' G))) \/ {(( 'not' F) '&' ( 'not' G))}) \/ {(F 'or' G)}) by ZF_LANG: 83

      .= (((( Subformulae ( 'not' F)) \/ (( Subformulae G) \/ {( 'not' G)})) \/ {(( 'not' F) '&' ( 'not' G))}) \/ {(F 'or' G)}) by ZF_LANG: 82

      .= ((((( Subformulae F) \/ {( 'not' F)}) \/ (( Subformulae G) \/ {( 'not' G)})) \/ {(( 'not' F) '&' ( 'not' G))}) \/ {(F 'or' G)}) by ZF_LANG: 82

      .= (((( Subformulae F) \/ ((( Subformulae G) \/ {( 'not' G)}) \/ {( 'not' F)})) \/ {(( 'not' F) '&' ( 'not' G))}) \/ {(F 'or' G)}) by XBOOLE_1: 4

      .= (((( Subformulae F) \/ (( Subformulae G) \/ ( {( 'not' G)} \/ {( 'not' F)}))) \/ {(( 'not' F) '&' ( 'not' G))}) \/ {(F 'or' G)}) by XBOOLE_1: 4

      .= (((( Subformulae F) \/ (( Subformulae G) \/ {( 'not' G), ( 'not' F)})) \/ {(( 'not' F) '&' ( 'not' G))}) \/ {(F 'or' G)}) by ENUMSET1: 1

      .= ((((( Subformulae F) \/ ( Subformulae G)) \/ {( 'not' G), ( 'not' F)}) \/ {(( 'not' F) '&' ( 'not' G))}) \/ {(F 'or' G)}) by XBOOLE_1: 4

      .= (((( Subformulae F) \/ ( Subformulae G)) \/ {( 'not' G), ( 'not' F)}) \/ ( {(( 'not' F) '&' ( 'not' G))} \/ {(F 'or' G)})) by XBOOLE_1: 4

      .= (((( Subformulae F) \/ ( Subformulae G)) \/ {( 'not' G), ( 'not' F)}) \/ {(( 'not' F) '&' ( 'not' G)), (F 'or' G)}) by ENUMSET1: 1

      .= ((( Subformulae F) \/ ( Subformulae G)) \/ ( {( 'not' G), ( 'not' F)} \/ {(( 'not' F) '&' ( 'not' G)), (F 'or' G)})) by XBOOLE_1: 4

      .= ((( Subformulae F) \/ ( Subformulae G)) \/ {( 'not' G), ( 'not' F), (( 'not' F) '&' ( 'not' G)), (F 'or' G)}) by ENUMSET1: 5;

    end;

    theorem :: ZF_LANG1:57

    ( Subformulae (F <=> G)) = ((( Subformulae F) \/ ( Subformulae G)) \/ {( 'not' G), (F '&' ( 'not' G)), (F => G), ( 'not' F), (G '&' ( 'not' F)), (G => F), (F <=> G)})

    proof

      

      thus ( Subformulae (F <=> G)) = ((( Subformulae (F => G)) \/ ( Subformulae (G => F))) \/ {(F <=> G)}) by ZF_LANG: 83

      .= ((((( Subformulae F) \/ ( Subformulae G)) \/ {( 'not' G), (F '&' ( 'not' G)), (F => G)}) \/ ( Subformulae (G => F))) \/ {(F <=> G)}) by Th55

      .= ((((( Subformulae F) \/ ( Subformulae G)) \/ {( 'not' G), (F '&' ( 'not' G)), (F => G)}) \/ ((( Subformulae F) \/ ( Subformulae G)) \/ {( 'not' F), (G '&' ( 'not' F)), (G => F)})) \/ {(F <=> G)}) by Th55

      .= (((( Subformulae F) \/ ( Subformulae G)) \/ (((( Subformulae F) \/ ( Subformulae G)) \/ {( 'not' G), (F '&' ( 'not' G)), (F => G)}) \/ {( 'not' F), (G '&' ( 'not' F)), (G => F)})) \/ {(F <=> G)}) by XBOOLE_1: 4

      .= (((( Subformulae F) \/ ( Subformulae G)) \/ ((( Subformulae F) \/ ( Subformulae G)) \/ ( {( 'not' G), (F '&' ( 'not' G)), (F => G)} \/ {( 'not' F), (G '&' ( 'not' F)), (G => F)}))) \/ {(F <=> G)}) by XBOOLE_1: 4

      .= ((((( Subformulae F) \/ ( Subformulae G)) \/ (( Subformulae F) \/ ( Subformulae G))) \/ ( {( 'not' G), (F '&' ( 'not' G)), (F => G)} \/ {( 'not' F), (G '&' ( 'not' F)), (G => F)})) \/ {(F <=> G)}) by XBOOLE_1: 4

      .= (((( Subformulae F) \/ ( Subformulae G)) \/ {( 'not' G), (F '&' ( 'not' G)), (F => G), ( 'not' F), (G '&' ( 'not' F)), (G => F)}) \/ {(F <=> G)}) by ENUMSET1: 13

      .= ((( Subformulae F) \/ ( Subformulae G)) \/ ( {( 'not' G), (F '&' ( 'not' G)), (F => G), ( 'not' F), (G '&' ( 'not' F)), (G => F)} \/ {(F <=> G)})) by XBOOLE_1: 4

      .= ((( Subformulae F) \/ ( Subformulae G)) \/ {( 'not' G), (F '&' ( 'not' G)), (F => G), ( 'not' F), (G '&' ( 'not' F)), (G => F), (F <=> G)}) by ENUMSET1: 21;

    end;

    theorem :: ZF_LANG1:58

    

     Th58: ( Free (x '=' y)) = {x, y}

    proof

      

       A1: ( Var2 (x '=' y)) = y by Th1;

      (x '=' y) is being_equality & ( Var1 (x '=' y)) = x by Th1;

      hence thesis by A1, ZF_MODEL: 1;

    end;

    theorem :: ZF_LANG1:59

    

     Th59: ( Free (x 'in' y)) = {x, y}

    proof

      

       A1: ( Var2 (x 'in' y)) = y by Th2;

      (x 'in' y) is being_membership & ( Var1 (x 'in' y)) = x by Th2;

      hence thesis by A1, ZF_MODEL: 1;

    end;

    theorem :: ZF_LANG1:60

    

     Th60: ( Free ( 'not' p)) = ( Free p)

    proof

      ( 'not' p) is negative & ( the_argument_of ( 'not' p)) = p by Th3;

      hence thesis by ZF_MODEL: 1;

    end;

    theorem :: ZF_LANG1:61

    

     Th61: ( Free (p '&' q)) = (( Free p) \/ ( Free q))

    proof

      

       A1: ( the_right_argument_of (p '&' q)) = q by Th4;

      (p '&' q) is conjunctive & ( the_left_argument_of (p '&' q)) = p by Th4;

      hence thesis by A1, ZF_MODEL: 1;

    end;

    theorem :: ZF_LANG1:62

    

     Th62: ( Free ( All (x,p))) = (( Free p) \ {x})

    proof

      

       A1: ( the_scope_of ( All (x,p))) = p by Th8;

      ( All (x,p)) is universal & ( bound_in ( All (x,p))) = x by Th8;

      hence thesis by A1, ZF_MODEL: 1;

    end;

    theorem :: ZF_LANG1:63

    ( Free (p 'or' q)) = (( Free p) \/ ( Free q))

    proof

      

      thus ( Free (p 'or' q)) = ( Free (( 'not' p) '&' ( 'not' q))) by Th60

      .= (( Free ( 'not' p)) \/ ( Free ( 'not' q))) by Th61

      .= (( Free p) \/ ( Free ( 'not' q))) by Th60

      .= (( Free p) \/ ( Free q)) by Th60;

    end;

    theorem :: ZF_LANG1:64

    

     Th64: ( Free (p => q)) = (( Free p) \/ ( Free q))

    proof

      

      thus ( Free (p => q)) = ( Free (p '&' ( 'not' q))) by Th60

      .= (( Free p) \/ ( Free ( 'not' q))) by Th61

      .= (( Free p) \/ ( Free q)) by Th60;

    end;

    theorem :: ZF_LANG1:65

    ( Free (p <=> q)) = (( Free p) \/ ( Free q))

    proof

      

      thus ( Free (p <=> q)) = (( Free (p => q)) \/ ( Free (q => p))) by Th61

      .= ((( Free p) \/ ( Free q)) \/ ( Free (q => p))) by Th64

      .= ((( Free p) \/ ( Free q)) \/ (( Free q) \/ ( Free p))) by Th64

      .= (((( Free p) \/ ( Free q)) \/ ( Free q)) \/ ( Free p)) by XBOOLE_1: 4

      .= ((( Free p) \/ (( Free q) \/ ( Free q))) \/ ( Free p)) by XBOOLE_1: 4

      .= ((( Free p) \/ ( Free p)) \/ ( Free q)) by XBOOLE_1: 4

      .= (( Free p) \/ ( Free q));

    end;

    theorem :: ZF_LANG1:66

    

     Th66: ( Free ( Ex (x,p))) = (( Free p) \ {x})

    proof

      

      thus ( Free ( Ex (x,p))) = ( Free ( All (x,( 'not' p)))) by Th60

      .= (( Free ( 'not' p)) \ {x}) by Th62

      .= (( Free p) \ {x}) by Th60;

    end;

    theorem :: ZF_LANG1:67

    

     Th67: ( Free ( All (x,y,p))) = (( Free p) \ {x, y})

    proof

      

      thus ( Free ( All (x,y,p))) = (( Free ( All (y,p))) \ {x}) by Th62

      .= ((( Free p) \ {y}) \ {x}) by Th62

      .= (( Free p) \ ( {x} \/ {y})) by XBOOLE_1: 41

      .= (( Free p) \ {x, y}) by ENUMSET1: 1;

    end;

    theorem :: ZF_LANG1:68

    ( Free ( All (x,y,z,p))) = (( Free p) \ {x, y, z})

    proof

      

      thus ( Free ( All (x,y,z,p))) = (( Free ( All (y,z,p))) \ {x}) by Th62

      .= ((( Free p) \ {y, z}) \ {x}) by Th67

      .= (( Free p) \ ( {x} \/ {y, z})) by XBOOLE_1: 41

      .= (( Free p) \ {x, y, z}) by ENUMSET1: 2;

    end;

    theorem :: ZF_LANG1:69

    

     Th69: ( Free ( Ex (x,y,p))) = (( Free p) \ {x, y})

    proof

      

      thus ( Free ( Ex (x,y,p))) = (( Free ( Ex (y,p))) \ {x}) by Th66

      .= ((( Free p) \ {y}) \ {x}) by Th66

      .= (( Free p) \ ( {x} \/ {y})) by XBOOLE_1: 41

      .= (( Free p) \ {x, y}) by ENUMSET1: 1;

    end;

    theorem :: ZF_LANG1:70

    ( Free ( Ex (x,y,z,p))) = (( Free p) \ {x, y, z})

    proof

      

      thus ( Free ( Ex (x,y,z,p))) = (( Free ( Ex (y,z,p))) \ {x}) by Th66

      .= ((( Free p) \ {y, z}) \ {x}) by Th69

      .= (( Free p) \ ( {x} \/ {y, z})) by XBOOLE_1: 41

      .= (( Free p) \ {x, y, z}) by ENUMSET1: 2;

    end;

    scheme :: ZF_LANG1:sch1

    ZFInduction { P[ ZF-formula] } :

for H holds P[H]

      provided

       A1: for x1, x2 holds P[(x1 '=' x2)] & P[(x1 'in' x2)]

       and

       A2: for H st P[H] holds P[( 'not' H)]

       and

       A3: for H1, H2 st P[H1] & P[H2] holds P[(H1 '&' H2)]

       and

       A4: for H, x st P[H] holds P[( All (x,H))];

      

       A5: for H st H is conjunctive & P[( the_left_argument_of H)] & P[( the_right_argument_of H)] holds P[H]

      proof

        let H;

        assume H is conjunctive;

        then H = (( the_left_argument_of H) '&' ( the_right_argument_of H)) by ZF_LANG: 40;

        hence thesis by A3;

      end;

      

       A6: for H st H is atomic holds P[H]

      proof

        let H such that

         A7: H is being_equality or H is being_membership;

        

         A8: H is being_membership implies thesis by A1;

        H is being_equality implies thesis by A1;

        hence thesis by A7, A8;

      end;

      

       A9: for H st H is universal & P[( the_scope_of H)] holds P[H]

      proof

        let H;

        assume H is universal;

        then H = ( All (( bound_in H),( the_scope_of H))) by ZF_LANG: 44;

        hence thesis by A4;

      end;

      

       A10: for H st H is negative & P[( the_argument_of H)] holds P[H]

      proof

        let H;

        assume H is negative;

        then H = ( 'not' ( the_argument_of H)) by ZF_LANG:def 30;

        hence thesis by A2;

      end;

      thus for H holds P[H] from ZF_LANG:sch 1( A6, A10, A5, A9);

    end;

    reserve M for non empty set,

m,m9 for Element of M,

v,v9 for Function of VAR , M;

    definition

      let D,D1,D2 be non empty set, f be Function of D, D1;

      assume

       A1: D1 c= D2;

      :: ZF_LANG1:def1

      func D2 ! f -> Function of D, D2 equals f;

      correctness

      proof

        ( rng f) c= D1 by RELAT_1:def 19;

        then

         A2: ( rng f) c= D2 by A1;

        ( dom f) = D by FUNCT_2:def 1;

        hence thesis by A2, FUNCT_2:def 1, RELSET_1: 4;

      end;

    end

    notation

      let E be non empty set, f be Function of VAR , E, x be Variable, e be Element of E;

      synonym f / (x,e) for f +* (x,e);

    end

    definition

      let E be non empty set, f be Function of VAR , E, x be Variable, e be Element of E;

      :: original: /

      redefine

      func f / (x,e) -> Function of VAR , E ;

      coherence

      proof

        (f +* (x,e)) is Function of VAR , E;

        hence thesis;

      end;

    end

    theorem :: ZF_LANG1:71

    

     Th71: (M,v) |= ( All (x,H)) iff for m holds (M,(v / (x,m))) |= H

    proof

      thus (M,v) |= ( All (x,H)) implies for m holds (M,(v / (x,m))) |= H

      proof

        assume

         A1: (M,v) |= ( All (x,H));

        let m;

        for y st ((v / (x,m)) . y) <> (v . y) holds x = y by FUNCT_7: 32;

        hence thesis by A1, ZF_MODEL: 16;

      end;

      assume

       A2: for m holds (M,(v / (x,m))) |= H;

      now

        let v9;

        assume for y st (v9 . y) <> (v . y) holds x = y;

        then v9 = (v / (x,(v9 . x))) by FUNCT_7: 129;

        hence (M,v9) |= H by A2;

      end;

      hence thesis by ZF_MODEL: 16;

    end;

    theorem :: ZF_LANG1:72

    

     Th72: (M,v) |= ( All (x,H)) iff (M,(v / (x,m))) |= ( All (x,H))

    proof

      

       A1: for v, m st (M,v) |= ( All (x,H)) holds (M,(v / (x,m))) |= ( All (x,H))

      proof

        let v, m such that

         A2: (M,v) |= ( All (x,H));

        now

          let m9;

          ((v / (x,m)) / (x,m9)) = (v / (x,m9)) by FUNCT_7: 34;

          hence (M,((v / (x,m)) / (x,m9))) |= H by A2, Th71;

        end;

        hence thesis by Th71;

      end;

      ((v / (x,m)) / (x,(v . x))) = (v / (x,(v . x))) by FUNCT_7: 34

      .= v by FUNCT_7: 35;

      hence thesis by A1;

    end;

    theorem :: ZF_LANG1:73

    

     Th73: (M,v) |= ( Ex (x,H)) iff ex m st (M,(v / (x,m))) |= H

    proof

      thus (M,v) |= ( Ex (x,H)) implies ex m st (M,(v / (x,m))) |= H

      proof

        assume (M,v) |= ( Ex (x,H));

        then

        consider v9 such that

         A1: (for y st (v9 . y) <> (v . y) holds x = y) & (M,v9) |= H by ZF_MODEL: 20;

        take (v9 . x);

        thus thesis by A1, FUNCT_7: 129;

      end;

      given m such that

       A2: (M,(v / (x,m))) |= H;

      now

        take v9 = (v / (x,m));

        thus for y st (v9 . y) <> (v . y) holds x = y by FUNCT_7: 32;

        thus (M,v9) |= H by A2;

      end;

      hence thesis by ZF_MODEL: 20;

    end;

    theorem :: ZF_LANG1:74

    (M,v) |= ( Ex (x,H)) iff (M,(v / (x,m))) |= ( Ex (x,H))

    proof

      

       A1: for v, m st (M,v) |= ( Ex (x,H)) holds (M,(v / (x,m))) |= ( Ex (x,H))

      proof

        let v, m;

        assume (M,v) |= ( Ex (x,H));

        then

        consider m9 such that

         A2: (M,(v / (x,m9))) |= H by Th73;

        ((v / (x,m)) / (x,m9)) = (v / (x,m9)) by FUNCT_7: 34;

        hence thesis by A2, Th73;

      end;

      ((v / (x,m)) / (x,(v . x))) = (v / (x,(v . x))) by FUNCT_7: 34

      .= v by FUNCT_7: 35;

      hence thesis by A1;

    end;

    theorem :: ZF_LANG1:75

    for v, v9 st for x st x in ( Free H) holds (v9 . x) = (v . x) holds (M,v) |= H implies (M,v9) |= H

    proof

      defpred Etha[ ZF-formula] means for v, v9 st for x st x in ( Free $1) holds (v9 . x) = (v . x) holds (M,v) |= $1 implies (M,v9) |= $1;

      

       A1: for H1, H2 st Etha[H1] & Etha[H2] holds Etha[(H1 '&' H2)]

      proof

        let H1, H2 such that

         A2: Etha[H1] and

         A3: Etha[H2];

        let v, v9;

        assume

         A4: for x st x in ( Free (H1 '&' H2)) holds (v9 . x) = (v . x);

        

         A5: ( Free (H1 '&' H2)) = (( Free H1) \/ ( Free H2)) by Th61;

         A6:

        now

          let x;

          assume x in ( Free H2);

          then x in ( Free (H1 '&' H2)) by A5, XBOOLE_0:def 3;

          hence (v9 . x) = (v . x) by A4;

        end;

        assume

         A7: (M,v) |= (H1 '&' H2);

        then (M,v) |= H2 by ZF_MODEL: 15;

        then

         A8: (M,v9) |= H2 by A3, A6;

         A9:

        now

          let x;

          assume x in ( Free H1);

          then x in ( Free (H1 '&' H2)) by A5, XBOOLE_0:def 3;

          hence (v9 . x) = (v . x) by A4;

        end;

        (M,v) |= H1 by A7, ZF_MODEL: 15;

        then (M,v9) |= H1 by A2, A9;

        hence thesis by A8, ZF_MODEL: 15;

      end;

      

       A10: for x1, x2 holds Etha[(x1 '=' x2)] & Etha[(x1 'in' x2)]

      proof

        let x1, x2;

        

         A11: ( Free (x1 '=' x2)) = {x1, x2} by Th58;

        thus Etha[(x1 '=' x2)]

        proof

          let v, v9;

          assume

           A12: for x st x in ( Free (x1 '=' x2)) holds (v9 . x) = (v . x);

          x2 in ( Free (x1 '=' x2)) by A11, TARSKI:def 2;

          then

           A13: (v9 . x2) = (v . x2) by A12;

          assume (M,v) |= (x1 '=' x2);

          then

           A14: (v . x1) = (v . x2) by ZF_MODEL: 12;

          x1 in ( Free (x1 '=' x2)) by A11, TARSKI:def 2;

          then (v9 . x1) = (v . x1) by A12;

          hence thesis by A14, A13, ZF_MODEL: 12;

        end;

        let v, v9;

        assume

         A15: for x st x in ( Free (x1 'in' x2)) holds (v9 . x) = (v . x);

        

         A16: ( Free (x1 'in' x2)) = {x1, x2} by Th59;

        then x2 in ( Free (x1 'in' x2)) by TARSKI:def 2;

        then

         A17: (v9 . x2) = (v . x2) by A15;

        assume (M,v) |= (x1 'in' x2);

        then

         A18: (v . x1) in (v . x2) by ZF_MODEL: 13;

        x1 in ( Free (x1 'in' x2)) by A16, TARSKI:def 2;

        then (v9 . x1) = (v . x1) by A15;

        hence thesis by A18, A17, ZF_MODEL: 13;

      end;

      

       A19: for H, x st Etha[H] holds Etha[( All (x,H))]

      proof

        let H, x1 such that

         A20: Etha[H];

        let v, v9;

        assume that

         A21: for x st x in ( Free ( All (x1,H))) holds (v9 . x) = (v . x) and

         A22: (M,v) |= ( All (x1,H));

        now

          let m;

          

           A23: ( Free ( All (x1,H))) = (( Free H) \ {x1}) by Th62;

           A24:

          now

            let x;

            assume x in ( Free H);

            then x in ( Free ( All (x1,H))) & not x in {x1} or x in {x1} by A23, XBOOLE_0:def 5;

            then (v9 . x) = (v . x) & x <> x1 or x = x1 by A21, TARSKI:def 1;

            then ((v9 / (x1,m)) . x) = (v . x) & (v . x) = ((v / (x1,m)) . x) or ((v / (x1,m)) . x) = m & ((v9 / (x1,m)) . x) = m by FUNCT_7: 32, FUNCT_7: 128;

            hence ((v9 / (x1,m)) . x) = ((v / (x1,m)) . x);

          end;

          (M,(v / (x1,m))) |= H by A22, Th71;

          hence (M,(v9 / (x1,m))) |= H by A20, A24;

        end;

        hence thesis by Th71;

      end;

      

       A25: for H st Etha[H] holds Etha[( 'not' H)]

      proof

        let H such that

         A26: Etha[H];

        let v, v9;

        assume

         A27: for x st x in ( Free ( 'not' H)) holds (v9 . x) = (v . x);

         A28:

        now

          let x;

          assume x in ( Free H);

          then x in ( Free ( 'not' H)) by Th60;

          hence (v . x) = (v9 . x) by A27;

        end;

        assume (M,v) |= ( 'not' H);

        then not (M,v) |= H by ZF_MODEL: 14;

        then not (M,v9) |= H by A26, A28;

        hence thesis by ZF_MODEL: 14;

      end;

      for H holds Etha[H] from ZFInduction( A10, A25, A1, A19);

      hence thesis;

    end;

    registration

      let H;

      cluster ( Free H) -> finite;

      coherence

      proof

        defpred P[ ZF-formula] means ( Free $1) is finite;

        

         A1: P[p] & P[q] implies P[(p '&' q)]

        proof

          ( Free (p '&' q)) = (( Free p) \/ ( Free q)) by Th61;

          hence thesis;

        end;

        

         A2: P[p] implies P[( All (x,p))]

        proof

          ( Free ( All (x,p))) = (( Free p) \ {x}) by Th62;

          hence thesis;

        end;

        

         A3: P[(x '=' y)] & P[(x 'in' y)]

        proof

          ( Free (x '=' y)) = {x, y} by Th58;

          hence thesis by Th59;

        end;

        

         A4: P[p] implies P[( 'not' p)] by Th60;

         P[p] from ZFInduction( A3, A4, A1, A2);

        hence thesis;

      end;

    end

    reserve i,j for Element of NAT ;

    theorem :: ZF_LANG1:76

    ( x. i) = ( x. j) implies i = j;

    theorem :: ZF_LANG1:77

    ex i st x = ( x. i)

    proof

      x in VAR ;

      then

      consider j such that

       A1: x = j and

       A2: 5 <= j;

      consider i be Nat such that

       A3: j = (5 + i) by A2, NAT_1: 10;

      reconsider i as Element of NAT by ORDINAL1:def 12;

      take i;

      thus thesis by A1, A3;

    end;

    theorem :: ZF_LANG1:78

    

     Th78: (M,v) |= (x '=' x)

    proof

      (v . x) = (v . x);

      hence thesis by ZF_MODEL: 12;

    end;

    theorem :: ZF_LANG1:79

    

     Th79: M |= (x '=' x) by Th78;

    theorem :: ZF_LANG1:80

    

     Th80: not (M,v) |= (x 'in' x)

    proof

       not (v . x) in (v . x);

      hence thesis by ZF_MODEL: 13;

    end;

    theorem :: ZF_LANG1:81

    

     Th81: not M |= (x 'in' x) & M |= ( 'not' (x 'in' x))

    proof

      set v = the Function of VAR , M;

       not (M,v) |= (x 'in' x) by Th80;

      hence not M |= (x 'in' x);

      let v;

       not (M,v) |= (x 'in' x) by Th80;

      hence thesis by ZF_MODEL: 14;

    end;

    theorem :: ZF_LANG1:82

    M |= (x '=' y) iff x = y or ex a st {a} = M

    proof

      thus M |= (x '=' y) implies x = y or ex a st {a} = M

      proof

        set v = the Function of VAR , M;

        set m = the Element of M;

        assume that

         A1: for v holds (M,v) |= (x '=' y) and

         A2: x <> y;

        reconsider a = m as set;

        take a;

        thus {a} c= M by ZFMISC_1: 31;

        let b be object;

        assume that

         A3: b in M and

         A4: not b in {a};

        reconsider b as Element of M by A3;

        (M,((v / (x,m)) / (y,b))) |= (x '=' y) by A1;

        then

         A5: (((v / (x,m)) / (y,b)) . x) = (((v / (x,m)) / (y,b)) . y) by ZF_MODEL: 12;

        

         A6: ((v / (x,m)) . x) = m & (((v / (x,m)) / (y,b)) . y) = b by FUNCT_7: 128;

        (((v / (x,m)) / (y,b)) . x) = ((v / (x,m)) . x) by A2, FUNCT_7: 32;

        hence contradiction by A4, A5, A6, TARSKI:def 1;

      end;

      now

        given a such that

         A7: {a} = M;

        let v;

        (v . x) = a & (v . y) = a by A7, TARSKI:def 1;

        hence (M,v) |= (x '=' y) by ZF_MODEL: 12;

      end;

      hence thesis by Th79;

    end;

    theorem :: ZF_LANG1:83

    M |= ( 'not' (x 'in' y)) iff x = y or for X st X in M holds X misses M

    proof

      thus M |= ( 'not' (x 'in' y)) implies x = y or for X st X in M holds X misses M

      proof

        set v = the Function of VAR , M;

        assume that

         A1: for v holds (M,v) |= ( 'not' (x 'in' y)) and

         A2: x <> y;

        let X;

        set a = the Element of (X /\ M);

        assume X in M;

        then

        reconsider m = X as Element of M;

        assume

         A3: (X /\ M) <> {} ;

        then

        reconsider a as Element of M by XBOOLE_0:def 4;

        (M,((v / (x,a)) / (y,m))) |= ( 'not' (x 'in' y)) by A1;

        then not (M,((v / (x,a)) / (y,m))) |= (x 'in' y) by ZF_MODEL: 14;

        then

         A4: not (((v / (x,a)) / (y,m)) . x) in (((v / (x,a)) / (y,m)) . y) by ZF_MODEL: 13;

        

         A5: ((v / (x,a)) . x) = a & (((v / (x,a)) / (y,m)) . y) = m by FUNCT_7: 128;

        (((v / (x,a)) / (y,m)) . x) = ((v / (x,a)) . x) by A2, FUNCT_7: 32;

        hence contradiction by A3, A4, A5, XBOOLE_0:def 4;

      end;

      now

        assume

         A6: for X st X in M holds X misses M;

        let v;

        (v . y) misses M by A6;

        then not (v . x) in (v . y) by XBOOLE_0: 3;

        then not (M,v) |= (x 'in' y) by ZF_MODEL: 13;

        hence (M,v) |= ( 'not' (x 'in' y)) by ZF_MODEL: 14;

      end;

      hence thesis by Th81;

    end;

    theorem :: ZF_LANG1:84

    H is being_equality implies ((M,v) |= H iff (v . ( Var1 H)) = (v . ( Var2 H)))

    proof

      assume H is being_equality;

      then H = (( Var1 H) '=' ( Var2 H)) by ZF_LANG: 36;

      hence thesis by ZF_MODEL: 12;

    end;

    theorem :: ZF_LANG1:85

    H is being_membership implies ((M,v) |= H iff (v . ( Var1 H)) in (v . ( Var2 H)))

    proof

      assume H is being_membership;

      then H = (( Var1 H) 'in' ( Var2 H)) by ZF_LANG: 37;

      hence thesis by ZF_MODEL: 13;

    end;

    theorem :: ZF_LANG1:86

    H is negative implies ((M,v) |= H iff not (M,v) |= ( the_argument_of H))

    proof

      assume H is negative;

      then H = ( 'not' ( the_argument_of H)) by ZF_LANG:def 30;

      hence thesis by ZF_MODEL: 14;

    end;

    theorem :: ZF_LANG1:87

    H is conjunctive implies ((M,v) |= H iff (M,v) |= ( the_left_argument_of H) & (M,v) |= ( the_right_argument_of H))

    proof

      assume H is conjunctive;

      then H = (( the_left_argument_of H) '&' ( the_right_argument_of H)) by ZF_LANG: 40;

      hence thesis by ZF_MODEL: 15;

    end;

    theorem :: ZF_LANG1:88

    H is universal implies ((M,v) |= H iff for m holds (M,(v / (( bound_in H),m))) |= ( the_scope_of H))

    proof

      assume H is universal;

      then H = ( All (( bound_in H),( the_scope_of H))) by ZF_LANG: 44;

      hence thesis by Th71;

    end;

    theorem :: ZF_LANG1:89

    H is disjunctive implies ((M,v) |= H iff (M,v) |= ( the_left_argument_of H) or (M,v) |= ( the_right_argument_of H))

    proof

      assume H is disjunctive;

      then H = (( the_left_argument_of H) 'or' ( the_right_argument_of H)) by ZF_LANG: 41;

      hence thesis by ZF_MODEL: 17;

    end;

    theorem :: ZF_LANG1:90

    H is conditional implies ((M,v) |= H iff ((M,v) |= ( the_antecedent_of H) implies (M,v) |= ( the_consequent_of H)))

    proof

      assume H is conditional;

      then H = (( the_antecedent_of H) => ( the_consequent_of H)) by ZF_LANG: 47;

      hence thesis by ZF_MODEL: 18;

    end;

    theorem :: ZF_LANG1:91

    H is biconditional implies ((M,v) |= H iff ((M,v) |= ( the_left_side_of H) iff (M,v) |= ( the_right_side_of H)))

    proof

      assume H is biconditional;

      then H = (( the_left_side_of H) <=> ( the_right_side_of H)) by ZF_LANG: 49;

      hence thesis by ZF_MODEL: 19;

    end;

    theorem :: ZF_LANG1:92

    H is existential implies ((M,v) |= H iff ex m st (M,(v / (( bound_in H),m))) |= ( the_scope_of H))

    proof

      assume H is existential;

      then H = ( Ex (( bound_in H),( the_scope_of H))) by ZF_LANG: 45;

      hence thesis by Th73;

    end;

    theorem :: ZF_LANG1:93

    M |= ( Ex (x,H)) iff for v holds ex m st (M,(v / (x,m))) |= H

    proof

      thus M |= ( Ex (x,H)) implies for v holds ex m st (M,(v / (x,m))) |= H by Th73;

      assume

       A1: for v holds ex m st (M,(v / (x,m))) |= H;

      let v;

      ex m st (M,(v / (x,m))) |= H by A1;

      hence thesis by Th73;

    end;

    theorem :: ZF_LANG1:94

    

     Th94: M |= H implies M |= ( Ex (x,H))

    proof

      assume

       A1: M |= H;

      let v;

      (M,(v / (x,(v . x)))) |= H by A1;

      hence thesis by Th73;

    end;

    theorem :: ZF_LANG1:95

    

     Th95: M |= H iff M |= ( All (x,y,H))

    proof

      M |= H iff M |= ( All (y,H)) by ZF_MODEL: 23;

      hence thesis by ZF_MODEL: 23;

    end;

    theorem :: ZF_LANG1:96

    

     Th96: M |= H implies M |= ( Ex (x,y,H))

    proof

      M |= H implies M |= ( Ex (y,H)) by Th94;

      hence thesis by Th94;

    end;

    theorem :: ZF_LANG1:97

    M |= H iff M |= ( All (x,y,z,H))

    proof

      M |= H iff M |= ( All (y,z,H)) by Th95;

      hence thesis by ZF_MODEL: 23;

    end;

    theorem :: ZF_LANG1:98

    M |= H implies M |= ( Ex (x,y,z,H))

    proof

      M |= H implies M |= ( Ex (y,z,H)) by Th96;

      hence thesis by Th94;

    end;

    theorem :: ZF_LANG1:99

    (M,v) |= ((p <=> q) => (p => q)) & M |= ((p <=> q) => (p => q))

    proof

       A1:

      now

        let v;

        (M,v) |= (p <=> q) implies (M,v) |= (p => q) by ZF_MODEL: 15;

        hence (M,v) |= ((p <=> q) => (p => q)) by ZF_MODEL: 18;

      end;

      hence (M,v) |= ((p <=> q) => (p => q));

      let v;

      thus thesis by A1;

    end;

    theorem :: ZF_LANG1:100

    (M,v) |= ((p <=> q) => (q => p)) & M |= ((p <=> q) => (q => p))

    proof

       A1:

      now

        let v;

        (M,v) |= (p <=> q) implies (M,v) |= (q => p) by ZF_MODEL: 15;

        hence (M,v) |= ((p <=> q) => (q => p)) by ZF_MODEL: 18;

      end;

      hence (M,v) |= ((p <=> q) => (q => p));

      let v;

      thus thesis by A1;

    end;

    theorem :: ZF_LANG1:101

    

     Th101: M |= ((p => q) => ((q => r) => (p => r)))

    proof

      let v;

      now

        assume

         A1: (M,v) |= (p => q);

        now

          assume

           A2: (M,v) |= (q => r);

          now

            assume (M,v) |= p;

            then (M,v) |= q by A1, ZF_MODEL: 18;

            hence (M,v) |= r by A2, ZF_MODEL: 18;

          end;

          hence (M,v) |= (p => r) by ZF_MODEL: 18;

        end;

        hence (M,v) |= ((q => r) => (p => r)) by ZF_MODEL: 18;

      end;

      hence thesis by ZF_MODEL: 18;

    end;

    theorem :: ZF_LANG1:102

    

     Th102: (M,v) |= (p => q) & (M,v) |= (q => r) implies (M,v) |= (p => r)

    proof

      assume that

       A1: (M,v) |= (p => q) and

       A2: (M,v) |= (q => r);

      M |= ((p => q) => ((q => r) => (p => r))) by Th101;

      then (M,v) |= ((p => q) => ((q => r) => (p => r)));

      then (M,v) |= ((q => r) => (p => r)) by A1, ZF_MODEL: 18;

      hence thesis by A2, ZF_MODEL: 18;

    end;

    theorem :: ZF_LANG1:103

    M |= (p => q) & M |= (q => r) implies M |= (p => r)

    proof

      assume

       A1: M |= (p => q) & M |= (q => r);

      let v;

      (M,v) |= (p => q) & (M,v) |= (q => r) by A1;

      hence thesis by Th102;

    end;

    theorem :: ZF_LANG1:104

    (M,v) |= (((p => q) '&' (q => r)) => (p => r)) & M |= (((p => q) '&' (q => r)) => (p => r))

    proof

      now

        let v;

        now

          assume (M,v) |= ((p => q) '&' (q => r));

          then (M,v) |= (p => q) & (M,v) |= (q => r) by ZF_MODEL: 15;

          hence (M,v) |= (p => r) by Th102;

        end;

        hence (M,v) |= (((p => q) '&' (q => r)) => (p => r)) by ZF_MODEL: 18;

      end;

      hence thesis;

    end;

    theorem :: ZF_LANG1:105

    (M,v) |= (p => (q => p)) & M |= (p => (q => p))

    proof

      now

        let v;

        (M,v) |= p implies (M,v) |= (q => p) by ZF_MODEL: 18;

        hence (M,v) |= (p => (q => p)) by ZF_MODEL: 18;

      end;

      hence thesis;

    end;

    theorem :: ZF_LANG1:106

    (M,v) |= ((p => (q => r)) => ((p => q) => (p => r))) & M |= ((p => (q => r)) => ((p => q) => (p => r)))

    proof

      now

        let v;

        now

          assume

           A1: (M,v) |= (p => (q => r));

          now

            assume (M,v) |= (p => q);

            then

             A2: (M,v) |= p implies (M,v) |= (q => r) & (M,v) |= q by A1, ZF_MODEL: 18;

            (M,v) |= q & (M,v) |= (q => r) implies (M,v) |= r by ZF_MODEL: 18;

            hence (M,v) |= (p => r) by A2, ZF_MODEL: 18;

          end;

          hence (M,v) |= ((p => q) => (p => r)) by ZF_MODEL: 18;

        end;

        hence (M,v) |= ((p => (q => r)) => ((p => q) => (p => r))) by ZF_MODEL: 18;

      end;

      hence thesis;

    end;

    theorem :: ZF_LANG1:107

    (M,v) |= ((p '&' q) => p) & M |= ((p '&' q) => p)

    proof

      now

        let v;

        (M,v) |= (p '&' q) implies (M,v) |= p by ZF_MODEL: 15;

        hence (M,v) |= ((p '&' q) => p) by ZF_MODEL: 18;

      end;

      hence thesis;

    end;

    theorem :: ZF_LANG1:108

    (M,v) |= ((p '&' q) => q) & M |= ((p '&' q) => q)

    proof

      now

        let v;

        (M,v) |= (p '&' q) implies (M,v) |= q by ZF_MODEL: 15;

        hence (M,v) |= ((p '&' q) => q) by ZF_MODEL: 18;

      end;

      hence thesis;

    end;

    theorem :: ZF_LANG1:109

    (M,v) |= ((p '&' q) => (q '&' p)) & M |= ((p '&' q) => (q '&' p))

    proof

      now

        let v;

        

         A1: (M,v) |= p & (M,v) |= q implies (M,v) |= (q '&' p) by ZF_MODEL: 15;

        (M,v) |= (p '&' q) implies (M,v) |= p & (M,v) |= q by ZF_MODEL: 15;

        hence (M,v) |= ((p '&' q) => (q '&' p)) by A1, ZF_MODEL: 18;

      end;

      hence thesis;

    end;

    theorem :: ZF_LANG1:110

    (M,v) |= (p => (p '&' p)) & M |= (p => (p '&' p))

    proof

      now

        let v;

        (M,v) |= p implies (M,v) |= (p '&' p) by ZF_MODEL: 15;

        hence (M,v) |= (p => (p '&' p)) by ZF_MODEL: 18;

      end;

      hence thesis;

    end;

    theorem :: ZF_LANG1:111

    (M,v) |= ((p => q) => ((p => r) => (p => (q '&' r)))) & M |= ((p => q) => ((p => r) => (p => (q '&' r))))

    proof

      now

        let v;

        now

          assume

           A1: (M,v) |= (p => q);

          now

            assume (M,v) |= (p => r);

            then (M,v) |= p implies (M,v) |= r & (M,v) |= q by A1, ZF_MODEL: 18;

            then (M,v) |= p implies (M,v) |= (q '&' r) by ZF_MODEL: 15;

            hence (M,v) |= (p => (q '&' r)) by ZF_MODEL: 18;

          end;

          hence (M,v) |= ((p => r) => (p => (q '&' r))) by ZF_MODEL: 18;

        end;

        hence (M,v) |= ((p => q) => ((p => r) => (p => (q '&' r)))) by ZF_MODEL: 18;

      end;

      hence thesis;

    end;

    theorem :: ZF_LANG1:112

    

     Th112: (M,v) |= (p => (p 'or' q)) & M |= (p => (p 'or' q))

    proof

      now

        let v;

        (M,v) |= p implies (M,v) |= (p 'or' q) by ZF_MODEL: 17;

        hence (M,v) |= (p => (p 'or' q)) by ZF_MODEL: 18;

      end;

      hence thesis;

    end;

    theorem :: ZF_LANG1:113

    (M,v) |= (q => (p 'or' q)) & M |= (q => (p 'or' q))

    proof

      now

        let v;

        (M,v) |= q implies (M,v) |= (p 'or' q) by ZF_MODEL: 17;

        hence (M,v) |= (q => (p 'or' q)) by ZF_MODEL: 18;

      end;

      hence thesis;

    end;

    theorem :: ZF_LANG1:114

    (M,v) |= ((p 'or' q) => (q 'or' p)) & M |= ((p 'or' q) => (q 'or' p))

    proof

      now

        let v;

        

         A1: (M,v) |= p or (M,v) |= q implies (M,v) |= (q 'or' p) by ZF_MODEL: 17;

        (M,v) |= (p 'or' q) implies (M,v) |= p or (M,v) |= q by ZF_MODEL: 17;

        hence (M,v) |= ((p 'or' q) => (q 'or' p)) by A1, ZF_MODEL: 18;

      end;

      hence thesis;

    end;

    theorem :: ZF_LANG1:115

    (M,v) |= (p => (p 'or' p)) & M |= (p => (p 'or' p)) by Th112;

    theorem :: ZF_LANG1:116

    (M,v) |= ((p => r) => ((q => r) => ((p 'or' q) => r))) & M |= ((p => r) => ((q => r) => ((p 'or' q) => r)))

    proof

      now

        let v;

        now

          assume

           A1: (M,v) |= (p => r);

          now

            assume (M,v) |= (q => r);

            then (M,v) |= p or (M,v) |= q implies (M,v) |= r by A1, ZF_MODEL: 18;

            then (M,v) |= (p 'or' q) implies (M,v) |= r by ZF_MODEL: 17;

            hence (M,v) |= ((p 'or' q) => r) by ZF_MODEL: 18;

          end;

          hence (M,v) |= ((q => r) => ((p 'or' q) => r)) by ZF_MODEL: 18;

        end;

        hence (M,v) |= ((p => r) => ((q => r) => ((p 'or' q) => r))) by ZF_MODEL: 18;

      end;

      hence thesis;

    end;

    theorem :: ZF_LANG1:117

    (M,v) |= (((p => r) '&' (q => r)) => ((p 'or' q) => r)) & M |= (((p => r) '&' (q => r)) => ((p 'or' q) => r))

    proof

      now

        let v;

        now

          assume (M,v) |= ((p => r) '&' (q => r));

          then (M,v) |= (p => r) & (M,v) |= (q => r) by ZF_MODEL: 15;

          then (M,v) |= p or (M,v) |= q implies (M,v) |= r by ZF_MODEL: 18;

          then (M,v) |= (p 'or' q) implies (M,v) |= r by ZF_MODEL: 17;

          hence (M,v) |= ((p 'or' q) => r) by ZF_MODEL: 18;

        end;

        hence (M,v) |= (((p => r) '&' (q => r)) => ((p 'or' q) => r)) by ZF_MODEL: 18;

      end;

      hence thesis;

    end;

    theorem :: ZF_LANG1:118

    (M,v) |= ((p => ( 'not' q)) => (q => ( 'not' p))) & M |= ((p => ( 'not' q)) => (q => ( 'not' p)))

    proof

      now

        let v;

        now

          assume (M,v) |= (p => ( 'not' q));

          then (M,v) |= p implies (M,v) |= ( 'not' q) by ZF_MODEL: 18;

          then (M,v) |= q implies (M,v) |= ( 'not' p) by ZF_MODEL: 14;

          hence (M,v) |= (q => ( 'not' p)) by ZF_MODEL: 18;

        end;

        hence (M,v) |= ((p => ( 'not' q)) => (q => ( 'not' p))) by ZF_MODEL: 18;

      end;

      hence thesis;

    end;

    theorem :: ZF_LANG1:119

    (M,v) |= (( 'not' p) => (p => q)) & M |= (( 'not' p) => (p => q))

    proof

      now

        let v;

        now

          assume (M,v) |= ( 'not' p);

          then not (M,v) |= p by ZF_MODEL: 14;

          hence (M,v) |= (p => q) by ZF_MODEL: 18;

        end;

        hence (M,v) |= (( 'not' p) => (p => q)) by ZF_MODEL: 18;

      end;

      hence thesis;

    end;

    theorem :: ZF_LANG1:120

    (M,v) |= (((p => q) '&' (p => ( 'not' q))) => ( 'not' p)) & M |= (((p => q) '&' (p => ( 'not' q))) => ( 'not' p))

    proof

      now

        let v;

        now

          assume (M,v) |= ((p => q) '&' (p => ( 'not' q)));

          then (M,v) |= (p => q) & (M,v) |= (p => ( 'not' q)) by ZF_MODEL: 15;

          then (M,v) |= p implies (M,v) |= q & (M,v) |= ( 'not' q) by ZF_MODEL: 18;

          hence (M,v) |= ( 'not' p) by ZF_MODEL: 14;

        end;

        hence (M,v) |= (((p => q) '&' (p => ( 'not' q))) => ( 'not' p)) by ZF_MODEL: 18;

      end;

      hence thesis;

    end;

    theorem :: ZF_LANG1:121

    M |= (p => q) & M |= p implies M |= q

    proof

      assume

       A1: M |= (p => q) & M |= p;

      let v;

      (M,v) |= (p => q) & (M,v) |= p by A1;

      hence thesis by ZF_MODEL: 18;

    end;

    theorem :: ZF_LANG1:122

    (M,v) |= (( 'not' (p '&' q)) => (( 'not' p) 'or' ( 'not' q))) & M |= (( 'not' (p '&' q)) => (( 'not' p) 'or' ( 'not' q)))

    proof

      now

        let v;

        now

          assume (M,v) |= ( 'not' (p '&' q));

          then not (M,v) |= (p '&' q) by ZF_MODEL: 14;

          then not (M,v) |= p or not (M,v) |= q by ZF_MODEL: 15;

          then (M,v) |= ( 'not' p) or (M,v) |= ( 'not' q) by ZF_MODEL: 14;

          hence (M,v) |= (( 'not' p) 'or' ( 'not' q)) by ZF_MODEL: 17;

        end;

        hence (M,v) |= (( 'not' (p '&' q)) => (( 'not' p) 'or' ( 'not' q))) by ZF_MODEL: 18;

      end;

      hence thesis;

    end;

    theorem :: ZF_LANG1:123

    (M,v) |= ((( 'not' p) 'or' ( 'not' q)) => ( 'not' (p '&' q))) & M |= ((( 'not' p) 'or' ( 'not' q)) => ( 'not' (p '&' q)))

    proof

      now

        let v;

        now

          assume (M,v) |= (( 'not' p) 'or' ( 'not' q));

          then (M,v) |= ( 'not' p) or (M,v) |= ( 'not' q) by ZF_MODEL: 17;

          then not (M,v) |= p or not (M,v) |= q by ZF_MODEL: 14;

          then not (M,v) |= (p '&' q) by ZF_MODEL: 15;

          hence (M,v) |= ( 'not' (p '&' q)) by ZF_MODEL: 14;

        end;

        hence (M,v) |= ((( 'not' p) 'or' ( 'not' q)) => ( 'not' (p '&' q))) by ZF_MODEL: 18;

      end;

      hence thesis;

    end;

    theorem :: ZF_LANG1:124

    (M,v) |= (( 'not' (p 'or' q)) => (( 'not' p) '&' ( 'not' q))) & M |= (( 'not' (p 'or' q)) => (( 'not' p) '&' ( 'not' q)))

    proof

      now

        let v;

        now

          assume (M,v) |= ( 'not' (p 'or' q));

          then

           A1: not (M,v) |= (p 'or' q) by ZF_MODEL: 14;

          then not (M,v) |= q by ZF_MODEL: 17;

          then

           A2: (M,v) |= ( 'not' q) by ZF_MODEL: 14;

           not (M,v) |= p by A1, ZF_MODEL: 17;

          then (M,v) |= ( 'not' p) by ZF_MODEL: 14;

          hence (M,v) |= (( 'not' p) '&' ( 'not' q)) by A2, ZF_MODEL: 15;

        end;

        hence (M,v) |= (( 'not' (p 'or' q)) => (( 'not' p) '&' ( 'not' q))) by ZF_MODEL: 18;

      end;

      hence thesis;

    end;

    theorem :: ZF_LANG1:125

    (M,v) |= ((( 'not' p) '&' ( 'not' q)) => ( 'not' (p 'or' q))) & M |= ((( 'not' p) '&' ( 'not' q)) => ( 'not' (p 'or' q)))

    proof

      now

        let v;

        now

          assume

           A1: (M,v) |= (( 'not' p) '&' ( 'not' q));

          then (M,v) |= ( 'not' q) by ZF_MODEL: 15;

          then

           A2: not (M,v) |= q by ZF_MODEL: 14;

          (M,v) |= ( 'not' p) by A1, ZF_MODEL: 15;

          then not (M,v) |= p by ZF_MODEL: 14;

          then not (M,v) |= (p 'or' q) by A2, ZF_MODEL: 17;

          hence (M,v) |= ( 'not' (p 'or' q)) by ZF_MODEL: 14;

        end;

        hence (M,v) |= ((( 'not' p) '&' ( 'not' q)) => ( 'not' (p 'or' q))) by ZF_MODEL: 18;

      end;

      hence thesis;

    end;

    theorem :: ZF_LANG1:126

    M |= (( All (x,H)) => H)

    proof

      let v;

      (M,v) |= ( All (x,H)) implies (M,(v / (x,(v . x)))) |= H by Th71;

      then (M,v) |= ( All (x,H)) implies (M,v) |= H by FUNCT_7: 35;

      hence thesis by ZF_MODEL: 18;

    end;

    theorem :: ZF_LANG1:127

    M |= (H => ( Ex (x,H)))

    proof

      let v;

      (M,(v / (x,(v . x)))) |= H implies (M,v) |= ( Ex (x,H)) by Th73;

      then (M,v) |= H implies (M,v) |= ( Ex (x,H)) by FUNCT_7: 35;

      hence thesis by ZF_MODEL: 18;

    end;

    theorem :: ZF_LANG1:128

    

     Th128: not x in ( Free H1) implies M |= (( All (x,(H1 => H2))) => (H1 => ( All (x,H2))))

    proof

      assume

       A1: not x in ( Free H1);

      let v;

      now

        assume

         A2: (M,v) |= ( All (x,(H1 => H2)));

        now

          assume

           A3: (M,v) |= H1;

          now

            let m;

            (M,v) |= ( All (x,H1)) by A1, A3, ZFMODEL1: 10;

            then

             A4: (M,(v / (x,m))) |= H1 by Th71;

            (M,(v / (x,m))) |= (H1 => H2) by A2, Th71;

            hence (M,(v / (x,m))) |= H2 by A4, ZF_MODEL: 18;

          end;

          hence (M,v) |= ( All (x,H2)) by Th71;

        end;

        hence (M,v) |= (H1 => ( All (x,H2))) by ZF_MODEL: 18;

      end;

      hence thesis by ZF_MODEL: 18;

    end;

    theorem :: ZF_LANG1:129

     not x in ( Free H1) & M |= (H1 => H2) implies M |= (H1 => ( All (x,H2)))

    proof

      assume that

       A1: not x in ( Free H1) and

       A2: for v holds (M,v) |= (H1 => H2);

      let v;

      M |= (( All (x,(H1 => H2))) => (H1 => ( All (x,H2)))) by A1, Th128;

      then

       A3: (M,v) |= (( All (x,(H1 => H2))) => (H1 => ( All (x,H2))));

      for m holds (M,(v / (x,m))) |= (H1 => H2) by A2;

      then (M,v) |= ( All (x,(H1 => H2))) by Th71;

      hence thesis by A3, ZF_MODEL: 18;

    end;

    theorem :: ZF_LANG1:130

    

     Th130: not x in ( Free H2) implies M |= (( All (x,(H1 => H2))) => (( Ex (x,H1)) => H2))

    proof

      assume

       A1: not x in ( Free H2);

      let v;

      now

        assume

         A2: (M,v) |= ( All (x,(H1 => H2)));

        now

          assume (M,v) |= ( Ex (x,H1));

          then

          consider m such that

           A3: (M,(v / (x,m))) |= H1 by Th73;

          (M,(v / (x,m))) |= (H1 => H2) by A2, Th71;

          then (M,(v / (x,m))) |= H2 by A3, ZF_MODEL: 18;

          then (M,(v / (x,m))) |= ( All (x,H2)) by A1, ZFMODEL1: 10;

          then (M,v) |= ( All (x,H2)) by Th72;

          then (M,(v / (x,(v . x)))) |= H2 by Th71;

          hence (M,v) |= H2 by FUNCT_7: 35;

        end;

        hence (M,v) |= (( Ex (x,H1)) => H2) by ZF_MODEL: 18;

      end;

      hence thesis by ZF_MODEL: 18;

    end;

    theorem :: ZF_LANG1:131

     not x in ( Free H2) & M |= (H1 => H2) implies M |= (( Ex (x,H1)) => H2)

    proof

      assume that

       A1: not x in ( Free H2) and

       A2: for v holds (M,v) |= (H1 => H2);

      let v;

      M |= (( All (x,(H1 => H2))) => (( Ex (x,H1)) => H2)) by A1, Th130;

      then

       A3: (M,v) |= (( All (x,(H1 => H2))) => (( Ex (x,H1)) => H2));

      for m holds (M,(v / (x,m))) |= (H1 => H2) by A2;

      then (M,v) |= ( All (x,(H1 => H2))) by Th71;

      hence thesis by A3, ZF_MODEL: 18;

    end;

    theorem :: ZF_LANG1:132

    M |= (H1 => ( All (x,H2))) implies M |= (H1 => H2)

    proof

      assume

       A1: for v holds (M,v) |= (H1 => ( All (x,H2)));

      let v;

      

       A2: (M,v) |= (H1 => ( All (x,H2))) by A1;

      now

        assume (M,v) |= H1;

        then (M,v) |= ( All (x,H2)) by A2, ZF_MODEL: 18;

        then (M,(v / (x,(v . x)))) |= H2 by Th71;

        hence (M,v) |= H2 by FUNCT_7: 35;

      end;

      hence thesis by ZF_MODEL: 18;

    end;

    theorem :: ZF_LANG1:133

    M |= (( Ex (x,H1)) => H2) implies M |= (H1 => H2)

    proof

      assume

       A1: for v holds (M,v) |= (( Ex (x,H1)) => H2);

      let v;

      

       A2: (M,v) |= (( Ex (x,H1)) => H2) by A1;

      now

        assume (M,v) |= H1;

        then (M,(v / (x,(v . x)))) |= H1 by FUNCT_7: 35;

        then (M,v) |= ( Ex (x,H1)) by Th73;

        hence (M,v) |= H2 by A2, ZF_MODEL: 18;

      end;

      hence thesis by ZF_MODEL: 18;

    end;

    theorem :: ZF_LANG1:134

     WFF c= ( bool [: NAT , NAT :])

    proof

      let a be object;

      assume a in WFF ;

      then

      reconsider H = a as ZF-formula by ZF_LANG: 4;

      H c= [: NAT , NAT :];

      hence thesis;

    end;

    definition

      let H;

      :: ZF_LANG1:def2

      func variables_in H -> set equals (( rng H) \ { 0 , 1, 2, 3, 4});

      correctness ;

    end

    theorem :: ZF_LANG1:135

    

     Th135: x <> 0 & x <> 1 & x <> 2 & x <> 3 & x <> 4

    proof

      x in VAR ;

      then

       A1: ex i st x = i & 5 <= i;

      assume x = 0 or x = 1 or x = 2 or x = 3 or x = 4;

      hence contradiction by A1;

    end;

    theorem :: ZF_LANG1:136

    

     Th136: not x in { 0 , 1, 2, 3, 4}

    proof

      assume x in { 0 , 1, 2, 3, 4};

      then x in ( { 0 , 1} \/ {2, 3, 4}) by ENUMSET1: 8;

      then x in { 0 , 1} or x in {2, 3, 4} by XBOOLE_0:def 3;

      then

       A1: x = 0 or x = 1 or x = 2 or x = 3 or x = 4 by ENUMSET1:def 1, TARSKI:def 2;

      x in VAR ;

      then ex i st x = i & 5 <= i;

      hence contradiction by A1;

    end;

    theorem :: ZF_LANG1:137

    

     Th137: a in ( variables_in H) implies a <> 0 & a <> 1 & a <> 2 & a <> 3 & a <> 4

    proof

      assume a in ( variables_in H);

      then not a in { 0 , 1, 2, 3, 4} by XBOOLE_0:def 5;

      then not a in ( { 0 , 1} \/ {2, 3, 4}) by ENUMSET1: 8;

      then ( not a in { 0 , 1}) & not a in {2, 3, 4} by XBOOLE_0:def 3;

      hence thesis by ENUMSET1:def 1, TARSKI:def 2;

    end;

    theorem :: ZF_LANG1:138

    

     Th138: ( variables_in (x '=' y)) = {x, y}

    proof

      

       A1: ( rng (x '=' y)) = (( rng ( <* 0 *> ^ <*x*>)) \/ ( rng <*y*>)) by FINSEQ_1: 31

      .= ((( rng <* 0 *>) \/ ( rng <*x*>)) \/ ( rng <*y*>)) by FINSEQ_1: 31

      .= (( { 0 } \/ ( rng <*x*>)) \/ ( rng <*y*>)) by FINSEQ_1: 39

      .= (( { 0 } \/ {x}) \/ ( rng <*y*>)) by FINSEQ_1: 39

      .= (( { 0 } \/ {x}) \/ {y}) by FINSEQ_1: 39

      .= ( { 0 } \/ ( {x} \/ {y})) by XBOOLE_1: 4

      .= ( { 0 } \/ {x, y}) by ENUMSET1: 1;

      thus ( variables_in (x '=' y)) c= {x, y}

      proof

        let a be object;

        assume

         A2: a in ( variables_in (x '=' y));

        then a <> 0 by Th137;

        then not a in { 0 } by TARSKI:def 1;

        hence thesis by A1, A2, XBOOLE_0:def 3;

      end;

      let a be object;

      assume

       A3: a in {x, y};

      then a = x or a = y by TARSKI:def 2;

      then

       A4: not a in { 0 , 1, 2, 3, 4} by Th136;

      a in ( { 0 } \/ {x, y}) by A3, XBOOLE_0:def 3;

      hence thesis by A1, A4, XBOOLE_0:def 5;

    end;

    theorem :: ZF_LANG1:139

    

     Th139: ( variables_in (x 'in' y)) = {x, y}

    proof

      

       A1: ( rng (x 'in' y)) = (( rng ( <*1*> ^ <*x*>)) \/ ( rng <*y*>)) by FINSEQ_1: 31

      .= ((( rng <*1*>) \/ ( rng <*x*>)) \/ ( rng <*y*>)) by FINSEQ_1: 31

      .= (( {1} \/ ( rng <*x*>)) \/ ( rng <*y*>)) by FINSEQ_1: 39

      .= (( {1} \/ {x}) \/ ( rng <*y*>)) by FINSEQ_1: 39

      .= (( {1} \/ {x}) \/ {y}) by FINSEQ_1: 39

      .= ( {1} \/ ( {x} \/ {y})) by XBOOLE_1: 4

      .= ( {1} \/ {x, y}) by ENUMSET1: 1;

      thus ( variables_in (x 'in' y)) c= {x, y}

      proof

        let a be object;

        assume

         A2: a in ( variables_in (x 'in' y));

        then a <> 1 by Th137;

        then not a in {1} by TARSKI:def 1;

        hence thesis by A1, A2, XBOOLE_0:def 3;

      end;

      let a be object;

      assume

       A3: a in {x, y};

      then a = x or a = y by TARSKI:def 2;

      then

       A4: not a in { 0 , 1, 2, 3, 4} by Th136;

      a in ( {1} \/ {x, y}) by A3, XBOOLE_0:def 3;

      hence thesis by A1, A4, XBOOLE_0:def 5;

    end;

    theorem :: ZF_LANG1:140

    

     Th140: ( variables_in ( 'not' H)) = ( variables_in H)

    proof

      

       A1: ( rng ( 'not' H)) = (( rng <*2*>) \/ ( rng H)) by FINSEQ_1: 31

      .= ( {2} \/ ( rng H)) by FINSEQ_1: 39;

      thus ( variables_in ( 'not' H)) c= ( variables_in H)

      proof

        let a be object;

        assume

         A2: a in ( variables_in ( 'not' H));

        then a <> 2 by Th137;

        then not a in {2} by TARSKI:def 1;

        then

         A3: a in ( rng H) by A1, A2, XBOOLE_0:def 3;

         not a in { 0 , 1, 2, 3, 4} by A2, XBOOLE_0:def 5;

        hence thesis by A3, XBOOLE_0:def 5;

      end;

      thus thesis by A1, XBOOLE_1: 7, XBOOLE_1: 33;

    end;

    theorem :: ZF_LANG1:141

    

     Th141: ( variables_in (H1 '&' H2)) = (( variables_in H1) \/ ( variables_in H2))

    proof

      

       A1: (( variables_in H1) \/ ( variables_in H2)) = ((( rng H1) \/ ( rng H2)) \ { 0 , 1, 2, 3, 4}) by XBOOLE_1: 42;

      

       A2: ( rng (H1 '&' H2)) = (( rng ( <*3*> ^ H1)) \/ ( rng H2)) by FINSEQ_1: 31

      .= ((( rng <*3*>) \/ ( rng H1)) \/ ( rng H2)) by FINSEQ_1: 31

      .= (( {3} \/ ( rng H1)) \/ ( rng H2)) by FINSEQ_1: 39

      .= ( {3} \/ (( rng H1) \/ ( rng H2))) by XBOOLE_1: 4;

      thus ( variables_in (H1 '&' H2)) c= (( variables_in H1) \/ ( variables_in H2))

      proof

        let a be object;

        assume

         A3: a in ( variables_in (H1 '&' H2));

        then a <> 3 by Th137;

        then not a in {3} by TARSKI:def 1;

        then

         A4: a in (( rng H1) \/ ( rng H2)) by A2, A3, XBOOLE_0:def 3;

         not a in { 0 , 1, 2, 3, 4} by A3, XBOOLE_0:def 5;

        hence thesis by A1, A4, XBOOLE_0:def 5;

      end;

      thus thesis by A2, A1, XBOOLE_1: 7, XBOOLE_1: 33;

    end;

    theorem :: ZF_LANG1:142

    

     Th142: ( variables_in ( All (x,H))) = (( variables_in H) \/ {x})

    proof

      

       A1: ( rng ( All (x,H))) = (( rng ( <*4*> ^ <*x*>)) \/ ( rng H)) by FINSEQ_1: 31

      .= ((( rng <*4*>) \/ ( rng <*x*>)) \/ ( rng H)) by FINSEQ_1: 31

      .= (( {4} \/ ( rng <*x*>)) \/ ( rng H)) by FINSEQ_1: 39

      .= (( {4} \/ {x}) \/ ( rng H)) by FINSEQ_1: 39

      .= ( {4} \/ ( {x} \/ ( rng H))) by XBOOLE_1: 4;

      thus ( variables_in ( All (x,H))) c= (( variables_in H) \/ {x})

      proof

        let a be object;

        assume

         A2: a in ( variables_in ( All (x,H)));

        then a <> 4 by Th137;

        then not a in {4} by TARSKI:def 1;

        then a in ( {x} \/ ( rng H)) by A1, A2, XBOOLE_0:def 3;

        then

         A3: a in {x} or a in ( rng H) by XBOOLE_0:def 3;

         not a in { 0 , 1, 2, 3, 4} by A2, XBOOLE_0:def 5;

        then a in ( rng H) implies a in ( variables_in H) by XBOOLE_0:def 5;

        hence thesis by A3, XBOOLE_0:def 3;

      end;

      let a be object;

      assume a in (( variables_in H) \/ {x});

      then

       A4: a in ( variables_in H) or a in {x} by XBOOLE_0:def 3;

      then a in ( {x} \/ ( rng H)) by XBOOLE_0:def 3;

      then

       A5: a in ( {4} \/ ( {x} \/ ( rng H))) by XBOOLE_0:def 3;

      a in ( rng H) & not a in { 0 , 1, 2, 3, 4} or a in {x} & x = a by A4, TARSKI:def 1, XBOOLE_0:def 5;

      then not a in { 0 , 1, 2, 3, 4} by Th136;

      hence thesis by A1, A5, XBOOLE_0:def 5;

    end;

    theorem :: ZF_LANG1:143

    ( variables_in (H1 'or' H2)) = (( variables_in H1) \/ ( variables_in H2))

    proof

      

      thus ( variables_in (H1 'or' H2)) = ( variables_in (( 'not' H1) '&' ( 'not' H2))) by Th140

      .= (( variables_in ( 'not' H1)) \/ ( variables_in ( 'not' H2))) by Th141

      .= (( variables_in H1) \/ ( variables_in ( 'not' H2))) by Th140

      .= (( variables_in H1) \/ ( variables_in H2)) by Th140;

    end;

    theorem :: ZF_LANG1:144

    

     Th144: ( variables_in (H1 => H2)) = (( variables_in H1) \/ ( variables_in H2))

    proof

      

      thus ( variables_in (H1 => H2)) = ( variables_in (H1 '&' ( 'not' H2))) by Th140

      .= (( variables_in H1) \/ ( variables_in ( 'not' H2))) by Th141

      .= (( variables_in H1) \/ ( variables_in H2)) by Th140;

    end;

    theorem :: ZF_LANG1:145

    ( variables_in (H1 <=> H2)) = (( variables_in H1) \/ ( variables_in H2))

    proof

      

      thus ( variables_in (H1 <=> H2)) = (( variables_in (H1 => H2)) \/ ( variables_in (H2 => H1))) by Th141

      .= ((( variables_in H1) \/ ( variables_in H2)) \/ ( variables_in (H2 => H1))) by Th144

      .= ((( variables_in H1) \/ ( variables_in H2)) \/ (( variables_in H1) \/ ( variables_in H2))) by Th144

      .= (( variables_in H1) \/ ( variables_in H2));

    end;

    theorem :: ZF_LANG1:146

    

     Th146: ( variables_in ( Ex (x,H))) = (( variables_in H) \/ {x})

    proof

      

      thus ( variables_in ( Ex (x,H))) = ( variables_in ( All (x,( 'not' H)))) by Th140

      .= (( variables_in ( 'not' H)) \/ {x}) by Th142

      .= (( variables_in H) \/ {x}) by Th140;

    end;

    theorem :: ZF_LANG1:147

    

     Th147: ( variables_in ( All (x,y,H))) = (( variables_in H) \/ {x, y})

    proof

      

      thus ( variables_in ( All (x,y,H))) = (( variables_in ( All (y,H))) \/ {x}) by Th142

      .= ((( variables_in H) \/ {y}) \/ {x}) by Th142

      .= (( variables_in H) \/ ( {y} \/ {x})) by XBOOLE_1: 4

      .= (( variables_in H) \/ {x, y}) by ENUMSET1: 1;

    end;

    theorem :: ZF_LANG1:148

    

     Th148: ( variables_in ( Ex (x,y,H))) = (( variables_in H) \/ {x, y})

    proof

      

      thus ( variables_in ( Ex (x,y,H))) = (( variables_in ( Ex (y,H))) \/ {x}) by Th146

      .= ((( variables_in H) \/ {y}) \/ {x}) by Th146

      .= (( variables_in H) \/ ( {y} \/ {x})) by XBOOLE_1: 4

      .= (( variables_in H) \/ {x, y}) by ENUMSET1: 1;

    end;

    theorem :: ZF_LANG1:149

    ( variables_in ( All (x,y,z,H))) = (( variables_in H) \/ {x, y, z})

    proof

      

      thus ( variables_in ( All (x,y,z,H))) = (( variables_in ( All (y,z,H))) \/ {x}) by Th142

      .= ((( variables_in H) \/ {y, z}) \/ {x}) by Th147

      .= (( variables_in H) \/ ( {y, z} \/ {x})) by XBOOLE_1: 4

      .= (( variables_in H) \/ {y, z, x}) by ENUMSET1: 3

      .= (( variables_in H) \/ {x, y, z}) by ENUMSET1: 59;

    end;

    theorem :: ZF_LANG1:150

    ( variables_in ( Ex (x,y,z,H))) = (( variables_in H) \/ {x, y, z})

    proof

      

      thus ( variables_in ( Ex (x,y,z,H))) = (( variables_in ( Ex (y,z,H))) \/ {x}) by Th146

      .= ((( variables_in H) \/ {y, z}) \/ {x}) by Th148

      .= (( variables_in H) \/ ( {y, z} \/ {x})) by XBOOLE_1: 4

      .= (( variables_in H) \/ {y, z, x}) by ENUMSET1: 3

      .= (( variables_in H) \/ {x, y, z}) by ENUMSET1: 59;

    end;

    theorem :: ZF_LANG1:151

    ( Free H) c= ( variables_in H)

    proof

      defpred P[ ZF-formula] means ( Free $1) c= ( variables_in $1);

      

       A1: P[H1] implies P[( 'not' H1)]

      proof

        assume ( Free H1) c= ( variables_in H1);

        then ( Free ( 'not' H1)) c= ( variables_in H1) by Th60;

        hence thesis by Th140;

      end;

      

       A2: P[H1] & P[H2] implies P[(H1 '&' H2)]

      proof

        assume ( Free H1) c= ( variables_in H1) & ( Free H2) c= ( variables_in H2);

        then (( Free H1) \/ ( Free H2)) c= (( variables_in H1) \/ ( variables_in H2)) by XBOOLE_1: 13;

        then ( Free (H1 '&' H2)) c= (( variables_in H1) \/ ( variables_in H2)) by Th61;

        hence thesis by Th141;

      end;

      

       A3: P[H1] implies P[( All (x,H1))]

      proof

        (( Free H1) \ {x}) c= ( Free H1) by XBOOLE_1: 36;

        then

         A4: ( Free ( All (x,H1))) c= ( Free H1) by Th62;

        ( variables_in H1) c= (( variables_in H1) \/ {x}) by XBOOLE_1: 7;

        then

         A5: ( variables_in H1) c= ( variables_in ( All (x,H1))) by Th142;

        assume ( Free H1) c= ( variables_in H1);

        then ( Free H1) c= ( variables_in ( All (x,H1))) by A5;

        hence thesis by A4, XBOOLE_1: 1;

      end;

      

       A6: P[(x '=' y)] & P[(x 'in' y)]

      proof

        ( variables_in (x '=' y)) = {x, y} & ( variables_in (x 'in' y)) = {x, y} by Th138, Th139;

        hence thesis by Th58, Th59;

      end;

      for H holds P[H] from ZFInduction( A6, A1, A2, A3);

      hence thesis;

    end;

    definition

      let H;

      :: original: variables_in

      redefine

      func variables_in H -> non empty Subset of VAR ;

      coherence

      proof

        defpred P[ ZF-formula] means ( variables_in $1) <> {} ;

        

         A1: for H1, H2 st P[H1] & P[H2] holds P[(H1 '&' H2)]

        proof

          let H1, H2;

          ( variables_in (H1 '&' H2)) = (( variables_in H1) \/ ( variables_in H2)) by Th141;

          hence thesis;

        end;

        

         A2: for H, x st P[H] holds P[( All (x,H))]

        proof

          let H, x;

          ( variables_in ( All (x,H))) = (( variables_in H) \/ {x}) by Th142;

          hence thesis;

        end;

        

         A3: for x, y holds P[(x '=' y)] & P[(x 'in' y)]

        proof

          let x, y;

          ( variables_in (x '=' y)) = {x, y} by Th138;

          hence thesis by Th139;

        end;

        

         A4: for H st P[H] holds P[( 'not' H)] by Th140;

        for H holds P[H] from ZFInduction( A3, A4, A1, A2);

        then

        reconsider D = ( variables_in H) as non empty set;

        D c= VAR

        proof

          let a be object;

          

           A5: ( rng H) c= NAT by FINSEQ_1:def 4;

          

           A6: ( 0 + 1) = 1;

          assume

           A7: a in D;

          then a in ( rng H);

          then

          reconsider i = a as Element of NAT by A5;

          a <> 0 by A7, Th137;

          then

           A8: 1 <= i by A6, NAT_1: 13;

          

           A9: (3 + 1) = 4;

          

           A10: (2 + 1) = 3;

          

           A11: (1 + 1) = 2;

          a <> 1 by A7, Th137;

          then 1 < i by A8, XXREAL_0: 1;

          then

           A12: 2 <= i by A11, NAT_1: 13;

          a <> 2 by A7, Th137;

          then 2 < i by A12, XXREAL_0: 1;

          then

           A13: 3 <= i by A10, NAT_1: 13;

          a <> 3 by A7, Th137;

          then 3 < i by A13, XXREAL_0: 1;

          then

           A14: 4 <= i by A9, NAT_1: 13;

          a <> 4 by A7, Th137;

          then

           A15: 4 < i by A14, XXREAL_0: 1;

          (4 + 1) = 5;

          then 5 <= i by A15, NAT_1: 13;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    definition

      let H, x, y;

      :: ZF_LANG1:def3

      func H / (x,y) -> Function means

      : Def3: ( dom it ) = ( dom H) & for a be object st a in ( dom H) holds ((H . a) = x implies (it . a) = y) & ((H . a) <> x implies (it . a) = (H . a));

      existence

      proof

        deffunc G( object) = (H . $1);

        deffunc F( object) = y;

        set A = ( dom H);

        defpred C[ object] means (H . $1) = x;

        thus ex f be Function st ( dom f) = A & for a be object st a in A holds ( C[a] implies (f . a) = F(a)) & ( not C[a] implies (f . a) = G(a)) from PARTFUN1:sch 1;

      end;

      uniqueness

      proof

        let f1,f2 be Function such that

         A1: ( dom f1) = ( dom H) and

         A2: for a be object st a in ( dom H) holds ((H . a) = x implies (f1 . a) = y) & ((H . a) <> x implies (f1 . a) = (H . a)) and

         A3: ( dom f2) = ( dom H) and

         A4: for a be object st a in ( dom H) holds ((H . a) = x implies (f2 . a) = y) & ((H . a) <> x implies (f2 . a) = (H . a));

        now

          let a be object;

          assume

           A5: a in ( dom H);

          then

           A6: (H . a) <> x implies (f1 . a) = (H . a) by A2;

          (H . a) = x implies (f1 . a) = y by A2, A5;

          hence (f1 . a) = (f2 . a) by A4, A5, A6;

        end;

        hence thesis by A1, A3, FUNCT_1: 2;

      end;

    end

    theorem :: ZF_LANG1:152

    

     Th152: ((x1 '=' x2) / (y1,y2)) = (z1 '=' z2) iff x1 <> y1 & x2 <> y1 & z1 = x1 & z2 = x2 or x1 = y1 & x2 <> y1 & z1 = y2 & z2 = x2 or x1 <> y1 & x2 = y1 & z1 = x1 & z2 = y2 or x1 = y1 & x2 = y1 & z1 = y2 & z2 = y2

    proof

      set H = (x1 '=' x2), Hz = (z1 '=' z2);

      set f = (H / (y1,y2));

      

       A1: (H . 1) = 0 & y1 <> 0 by Th135, ZF_LANG: 15;

      H is being_equality;

      then

       A2: H is atomic;

      then

       A3: ( len H) = 3 by ZF_LANG: 11;

      then

       A4: ( dom H) = {1, 2, 3} by FINSEQ_1:def 3, FINSEQ_3: 1;

      Hz is being_equality;

      then

       A5: Hz is atomic;

      then ( len Hz) = 3 by ZF_LANG: 11;

      then

       A6: ( dom Hz) = ( Seg 3) by FINSEQ_1:def 3;

      ( Var1 Hz) = z1 by Th1;

      then

       A7: (Hz . 2) = z1 by A5, ZF_LANG: 35;

      ( Var2 Hz) = z2 by Th1;

      then

       A8: (Hz . 3) = z2 by A5, ZF_LANG: 35;

      

       A9: ( Var2 H) = x2 by Th1;

      then

       A10: (H . 3) = x2 by A2, ZF_LANG: 35;

      

       A11: ( Var1 H) = x1 by Th1;

      then

       A12: (H . 2) = x1 by A2, ZF_LANG: 35;

      thus ((x1 '=' x2) / (y1,y2)) = (z1 '=' z2) implies x1 <> y1 & x2 <> y1 & z1 = x1 & z2 = x2 or x1 = y1 & x2 <> y1 & z1 = y2 & z2 = x2 or x1 <> y1 & x2 = y1 & z1 = x1 & z2 = y2 or x1 = y1 & x2 = y1 & z1 = y2 & z2 = y2

      proof

        assume

         A13: ((x1 '=' x2) / (y1,y2)) = (z1 '=' z2);

        per cases ;

          case

           A14: x1 <> y1 & x2 <> y1;

          2 in ( dom H) & 3 in ( dom H) by A4, ENUMSET1:def 1;

          hence thesis by A12, A10, A7, A8, A13, A14, Def3;

        end;

          case

           A15: x1 = y1 & x2 <> y1;

          

           A16: 2 in ( dom H) & 3 in ( dom H) by A4, ENUMSET1:def 1;

          (H . 2) = y1 by A2, A11, A15, ZF_LANG: 35;

          hence thesis by A10, A7, A8, A13, A15, A16, Def3;

        end;

          case

           A17: x1 <> y1 & x2 = y1;

          

           A18: 2 in ( dom H) & 3 in ( dom H) by A4, ENUMSET1:def 1;

          (H . 3) = y1 by A2, A9, A17, ZF_LANG: 35;

          hence thesis by A12, A7, A8, A13, A17, A18, Def3;

        end;

          case

           A19: x1 = y1 & x2 = y1;

          

           A20: 2 in ( dom H) & 3 in ( dom H) by A4, ENUMSET1:def 1;

          (H . 2) = y1 & (H . 3) = y1 by A2, A11, A9, A19, ZF_LANG: 35;

          hence thesis by A7, A8, A13, A20, Def3;

        end;

      end;

      

       A21: ( dom H) = ( Seg 3) by A3, FINSEQ_1:def 3;

      

       A22: ( dom f) = ( dom H) by Def3;

       A23:

      now

        assume

         A24: x1 <> y1 & x2 <> y1 & z1 = x1 & z2 = x2;

        now

          let a be object;

          assume

           A25: a in ( dom H);

          then a = 1 or a = 2 or a = 3 by A4, ENUMSET1:def 1;

          hence (Hz . a) = (f . a) by A12, A10, A1, A24, A25, Def3;

        end;

        hence f = Hz by A22, A21, A6, FUNCT_1: 2;

      end;

      

       A26: (Hz . 1) = 0 by ZF_LANG: 15;

       A27:

      now

        assume

         A28: x1 <> y1 & x2 = y1 & z1 = x1 & z2 = y2;

        now

          let a be object;

          assume

           A29: a in ( dom H);

          then a = 1 or a = 2 or a = 3 by A4, ENUMSET1:def 1;

          hence (Hz . a) = (f . a) by A12, A10, A26, A7, A8, A1, A28, A29, Def3;

        end;

        hence f = Hz by A22, A21, A6, FUNCT_1: 2;

      end;

       A30:

      now

        assume

         A31: x1 = y1 & x2 = y1 & z1 = y2 & z2 = y2;

        now

          let a be object;

          assume

           A32: a in ( dom H);

          then a = 1 or a = 2 or a = 3 by A4, ENUMSET1:def 1;

          hence (Hz . a) = (f . a) by A12, A10, A26, A7, A8, A1, A31, A32, Def3;

        end;

        hence f = Hz by A22, A21, A6, FUNCT_1: 2;

      end;

      now

        assume

         A33: x1 = y1 & x2 <> y1 & z1 = y2 & z2 = x2;

        now

          let a be object;

          assume

           A34: a in ( dom H);

          then a = 1 or a = 2 or a = 3 by A4, ENUMSET1:def 1;

          hence (Hz . a) = (f . a) by A12, A10, A26, A7, A8, A1, A33, A34, Def3;

        end;

        hence f = Hz by A22, A21, A6, FUNCT_1: 2;

      end;

      hence thesis by A23, A27, A30;

    end;

    theorem :: ZF_LANG1:153

    

     Th153: ex z1, z2 st ((x1 '=' x2) / (y1,y2)) = (z1 '=' z2)

    proof

      x1 <> y1 & x2 <> y1 or x1 = y1 & x2 <> y1 or x1 <> y1 & x2 = y1 or x1 = y1 & x2 = y1;

      then

      consider z1, z2 such that

       A1: x1 <> y1 & x2 <> y1 & z1 = x1 & z2 = x2 or x1 = y1 & x2 <> y1 & z1 = y2 & z2 = x2 or x1 <> y1 & x2 = y1 & z1 = x1 & z2 = y2 or x1 = y1 & x2 = y1 & z1 = y2 & z2 = y2;

      take z1, z2;

      thus thesis by A1, Th152;

    end;

    theorem :: ZF_LANG1:154

    

     Th154: ((x1 'in' x2) / (y1,y2)) = (z1 'in' z2) iff x1 <> y1 & x2 <> y1 & z1 = x1 & z2 = x2 or x1 = y1 & x2 <> y1 & z1 = y2 & z2 = x2 or x1 <> y1 & x2 = y1 & z1 = x1 & z2 = y2 or x1 = y1 & x2 = y1 & z1 = y2 & z2 = y2

    proof

      set H = (x1 'in' x2), Hz = (z1 'in' z2);

      set f = (H / (y1,y2));

      

       A1: (H . 1) = 1 & y1 <> 1 by Th135, ZF_LANG: 15;

      H is being_membership;

      then

       A2: H is atomic;

      then

       A3: ( len H) = 3 by ZF_LANG: 11;

      then

       A4: ( dom H) = {1, 2, 3} by FINSEQ_1:def 3, FINSEQ_3: 1;

      Hz is being_membership;

      then

       A5: Hz is atomic;

      then ( len Hz) = 3 by ZF_LANG: 11;

      then

       A6: ( dom Hz) = ( Seg 3) by FINSEQ_1:def 3;

      ( Var1 Hz) = z1 by Th2;

      then

       A7: (Hz . 2) = z1 by A5, ZF_LANG: 35;

      ( Var2 Hz) = z2 by Th2;

      then

       A8: (Hz . 3) = z2 by A5, ZF_LANG: 35;

      

       A9: ( Var2 H) = x2 by Th2;

      then

       A10: (H . 3) = x2 by A2, ZF_LANG: 35;

      

       A11: ( Var1 H) = x1 by Th2;

      then

       A12: (H . 2) = x1 by A2, ZF_LANG: 35;

      thus ((x1 'in' x2) / (y1,y2)) = (z1 'in' z2) implies x1 <> y1 & x2 <> y1 & z1 = x1 & z2 = x2 or x1 = y1 & x2 <> y1 & z1 = y2 & z2 = x2 or x1 <> y1 & x2 = y1 & z1 = x1 & z2 = y2 or x1 = y1 & x2 = y1 & z1 = y2 & z2 = y2

      proof

        assume

         A13: ((x1 'in' x2) / (y1,y2)) = (z1 'in' z2);

        per cases ;

          case

           A14: x1 <> y1 & x2 <> y1;

          2 in ( dom H) & 3 in ( dom H) by A4, ENUMSET1:def 1;

          hence thesis by A12, A10, A7, A8, A13, A14, Def3;

        end;

          case

           A15: x1 = y1 & x2 <> y1;

          

           A16: 2 in ( dom H) & 3 in ( dom H) by A4, ENUMSET1:def 1;

          (H . 2) = y1 by A2, A11, A15, ZF_LANG: 35;

          hence thesis by A10, A7, A8, A13, A15, A16, Def3;

        end;

          case

           A17: x1 <> y1 & x2 = y1;

          

           A18: 2 in ( dom H) & 3 in ( dom H) by A4, ENUMSET1:def 1;

          (H . 3) = y1 by A2, A9, A17, ZF_LANG: 35;

          hence thesis by A12, A7, A8, A13, A17, A18, Def3;

        end;

          case

           A19: x1 = y1 & x2 = y1;

          

           A20: 2 in ( dom H) & 3 in ( dom H) by A4, ENUMSET1:def 1;

          (H . 2) = y1 & (H . 3) = y1 by A2, A11, A9, A19, ZF_LANG: 35;

          hence thesis by A7, A8, A13, A20, Def3;

        end;

      end;

      

       A21: ( dom H) = ( Seg 3) by A3, FINSEQ_1:def 3;

      

       A22: ( dom f) = ( dom H) by Def3;

       A23:

      now

        assume

         A24: x1 <> y1 & x2 <> y1 & z1 = x1 & z2 = x2;

        now

          let a be object;

          assume

           A25: a in ( dom H);

          then a = 1 or a = 2 or a = 3 by A4, ENUMSET1:def 1;

          hence (Hz . a) = (f . a) by A12, A10, A1, A24, A25, Def3;

        end;

        hence f = Hz by A22, A21, A6, FUNCT_1: 2;

      end;

      

       A26: (Hz . 1) = 1 by ZF_LANG: 15;

       A27:

      now

        assume

         A28: x1 <> y1 & x2 = y1 & z1 = x1 & z2 = y2;

        now

          let a be object;

          assume

           A29: a in ( dom H);

          then a = 1 or a = 2 or a = 3 by A4, ENUMSET1:def 1;

          hence (Hz . a) = (f . a) by A12, A10, A26, A7, A8, A1, A28, A29, Def3;

        end;

        hence f = Hz by A22, A21, A6, FUNCT_1: 2;

      end;

       A30:

      now

        assume

         A31: x1 = y1 & x2 = y1 & z1 = y2 & z2 = y2;

        now

          let a be object;

          assume

           A32: a in ( dom H);

          then a = 1 or a = 2 or a = 3 by A4, ENUMSET1:def 1;

          hence (Hz . a) = (f . a) by A12, A10, A26, A7, A8, A1, A31, A32, Def3;

        end;

        hence f = Hz by A22, A21, A6, FUNCT_1: 2;

      end;

      now

        assume

         A33: x1 = y1 & x2 <> y1 & z1 = y2 & z2 = x2;

        now

          let a be object;

          assume

           A34: a in ( dom H);

          then a = 1 or a = 2 or a = 3 by A4, ENUMSET1:def 1;

          hence (Hz . a) = (f . a) by A12, A10, A26, A7, A8, A1, A33, A34, Def3;

        end;

        hence f = Hz by A22, A21, A6, FUNCT_1: 2;

      end;

      hence thesis by A23, A27, A30;

    end;

    theorem :: ZF_LANG1:155

    

     Th155: ex z1, z2 st ((x1 'in' x2) / (y1,y2)) = (z1 'in' z2)

    proof

      x1 <> y1 & x2 <> y1 or x1 = y1 & x2 <> y1 or x1 <> y1 & x2 = y1 or x1 = y1 & x2 = y1;

      then

      consider z1, z2 such that

       A1: x1 <> y1 & x2 <> y1 & z1 = x1 & z2 = x2 or x1 = y1 & x2 <> y1 & z1 = y2 & z2 = x2 or x1 <> y1 & x2 = y1 & z1 = x1 & z2 = y2 or x1 = y1 & x2 = y1 & z1 = y2 & z2 = y2;

      take z1, z2;

      thus thesis by A1, Th154;

    end;

    theorem :: ZF_LANG1:156

    

     Th156: ( 'not' F) = (( 'not' H) / (x,y)) iff F = (H / (x,y))

    proof

      set N = (( 'not' H) / (x,y));

      

       A1: ( len <*2*>) = 1 by FINSEQ_1: 39;

      

       A2: ( dom ( 'not' F)) = ( Seg ( len ( 'not' F))) & ( dom ( 'not' H)) = ( Seg ( len ( 'not' H))) by FINSEQ_1:def 3;

      

       A3: ( len ( 'not' F)) = (( len <*2*>) + ( len F)) & ( len ( 'not' H)) = (( len <*2*>) + ( len H)) by FINSEQ_1: 22;

      

       A4: ( dom F) = ( Seg ( len F)) & ( dom H) = ( Seg ( len H)) by FINSEQ_1:def 3;

      thus ( 'not' F) = (( 'not' H) / (x,y)) implies F = (H / (x,y))

      proof

        assume

         A5: ( 'not' F) = N;

        then

         A6: ( dom ( 'not' F)) = ( dom ( 'not' H)) by Def3;

        then

         A7: ( len ( 'not' F)) = ( len ( 'not' H)) by FINSEQ_3: 29;

         A8:

        now

          let a be object;

          assume

           A9: a in ( dom F);

          then

          reconsider i = a as Element of NAT ;

          

           A10: (F . a) = (N . (1 + i)) & (1 + i) in ( dom N) by A1, A5, A9, FINSEQ_1: 28, FINSEQ_1:def 7;

          

           A11: (( 'not' H) . (1 + i)) = (H . a) by A1, A4, A3, A7, A9, FINSEQ_1:def 7;

          then

           A12: (H . a) = x implies (F . a) = y by A5, A6, A10, Def3;

          

           A13: (H . a) <> x implies (F . a) = (H . a) by A5, A6, A10, A11, Def3;

          (H . a) = x implies ((H / (x,y)) . a) = y by A4, A3, A7, A9, Def3;

          hence (F . a) = ((H / (x,y)) . a) by A4, A3, A7, A9, A12, A13, Def3;

        end;

        

         A14: ( dom H) = ( dom (H / (x,y))) by Def3;

        ( dom F) = ( dom H) by A3, A7, FINSEQ_3: 29;

        hence thesis by A14, A8, FUNCT_1: 2;

      end;

      assume

       A15: F = (H / (x,y));

      then

       A16: ( dom F) = ( dom H) by Def3;

      then

       A17: ( len F) = ( len H) by FINSEQ_3: 29;

      

       A18: ( dom <*2*>) = {1} by FINSEQ_1: 2, FINSEQ_1:def 8;

       A19:

      now

        let a be object;

        assume

         A20: a in ( dom ( 'not' F));

        then

        reconsider i = a as Element of NAT ;

         A21:

        now

          

           A22: (( 'not' H) . a) <> x implies (N . a) = (( 'not' H) . a) by A2, A3, A17, A20, Def3;

          given j be Nat such that

           A23: j in ( dom F) and

           A24: i = (1 + j);

          

           A25: (H . j) = (( 'not' H) . i) & (F . j) = (( 'not' F) . i) by A1, A16, A23, A24, FINSEQ_1:def 7;

          then

           A26: (( 'not' H) . a) = x implies (( 'not' F) . a) = y by A15, A16, A23, Def3;

          (( 'not' H) . a) <> x implies (( 'not' F) . a) = (( 'not' H) . a) by A15, A16, A23, A25, Def3;

          hence (( 'not' F) . a) = (N . a) by A2, A3, A17, A20, A26, A22, Def3;

        end;

        now

          

           A27: (( 'not' H) . 1) = 2 & 2 <> x by Th135, FINSEQ_1: 41;

          assume i in {1};

          then

           A28: i = 1 by TARSKI:def 1;

          then (( 'not' F) . i) = 2 by FINSEQ_1: 41;

          hence (( 'not' F) . a) = (N . a) by A2, A3, A17, A20, A28, A27, Def3;

        end;

        hence (( 'not' F) . a) = (N . a) by A1, A18, A20, A21, FINSEQ_1: 25;

      end;

      ( dom ( 'not' F)) = ( dom N) by A2, A3, A17, Def3;

      hence thesis by A19, FUNCT_1: 2;

    end;

    

     Lm1: G1 = (H1 / (x,y)) & G2 = (H2 / (x,y)) implies (G1 '&' G2) = ((H1 '&' H2) / (x,y))

    proof

      set N = ((H1 '&' H2) / (x,y));

      

       A1: ( dom <*3*>) = {1} by FINSEQ_1: 2, FINSEQ_1:def 8;

      

       A2: ( dom (G1 '&' G2)) = ( Seg ( len (G1 '&' G2))) & ( dom (H1 '&' H2)) = ( Seg ( len (H1 '&' H2))) by FINSEQ_1:def 3;

      

       A3: ( len <*3*>) = 1 by FINSEQ_1: 39;

      then

       A4: ( len ( <*3*> ^ G1)) = (1 + ( len G1)) by FINSEQ_1: 22;

      then

       A5: ( len (G1 '&' G2)) = ((1 + ( len G1)) + ( len G2)) by FINSEQ_1: 22;

      

       A6: ( len ( <*3*> ^ H1)) = (1 + ( len H1)) by A3, FINSEQ_1: 22;

      then

       A7: ( len (H1 '&' H2)) = ((1 + ( len H1)) + ( len H2)) by FINSEQ_1: 22;

      

       A8: ( dom ( <*3*> ^ H1)) = ( Seg (1 + ( len H1))) by A6, FINSEQ_1:def 3;

      

       A9: ( dom N) = ( dom (H1 '&' H2)) by Def3;

      assume that

       A10: G1 = (H1 / (x,y)) and

       A11: G2 = (H2 / (x,y));

      

       A12: ( dom G1) = ( dom H1) by A10, Def3;

      then

       A13: ( len G1) = ( len H1) by FINSEQ_3: 29;

      

       A14: ( dom G2) = ( dom H2) by A11, Def3;

      then ( len G2) = ( len H2) by FINSEQ_3: 29;

      then

       A15: ( dom N) = ( dom (G1 '&' G2)) by A2, A5, A7, A13, Def3;

      

       A16: ( dom ( <*3*> ^ G1)) = ( Seg (1 + ( len G1))) by A4, FINSEQ_1:def 3;

      now

        let a be object;

        assume

         A17: a in ( dom N);

        then

        reconsider i = a as Element of NAT by A15;

         A18:

        now

           A19:

          now

            assume i in {1};

            then

             A20: i = 1 by TARSKI:def 1;

            ((H1 '&' H2) . 1) = 3 & x <> 3 by Th135, ZF_LANG: 16;

            then (N . i) = 3 by A9, A17, A20, Def3;

            hence (N . a) = ((G1 '&' G2) . a) by A20, ZF_LANG: 16;

          end;

          assume

           A21: i in ( dom ( <*3*> ^ G1));

          then

           A22: ((G1 '&' G2) . i) = (( <*3*> ^ G1) . i) & ((H1 '&' H2) . i) = (( <*3*> ^ H1) . i) by A16, A8, A13, FINSEQ_1:def 7;

          now

            

             A23: ((H1 '&' H2) . a) <> x implies (N . a) = ((H1 '&' H2) . a) by A9, A17, Def3;

            given j be Nat such that

             A24: j in ( dom G1) and

             A25: i = (1 + j);

            

             A26: (G1 . j) = ((G1 '&' G2) . i) & (H1 . j) = ((H1 '&' H2) . i) by A3, A12, A22, A24, A25, FINSEQ_1:def 7;

            then

             A27: ((H1 '&' H2) . a) = x implies ((G1 '&' G2) . a) = y by A10, A12, A24, Def3;

            ((H1 '&' H2) . a) <> x implies ((G1 '&' G2) . a) = ((H1 '&' H2) . a) by A10, A12, A24, A26, Def3;

            hence ((G1 '&' G2) . a) = (N . a) by A9, A17, A27, A23, Def3;

          end;

          hence ((G1 '&' G2) . a) = (N . a) by A3, A1, A21, A19, FINSEQ_1: 25;

        end;

        now

          

           A28: ((H1 '&' H2) . a) <> x implies (N . a) = ((H1 '&' H2) . a) by A9, A17, Def3;

          given j be Nat such that

           A29: j in ( dom G2) and

           A30: i = ((1 + ( len G1)) + j);

          

           A31: (G2 . j) = ((G1 '&' G2) . i) & (H2 . j) = ((H1 '&' H2) . i) by A4, A6, A14, A13, A29, A30, FINSEQ_1:def 7;

          then

           A32: ((H1 '&' H2) . a) = x implies ((G1 '&' G2) . a) = y by A11, A14, A29, Def3;

          ((H1 '&' H2) . a) <> x implies ((G1 '&' G2) . a) = ((H1 '&' H2) . a) by A11, A14, A29, A31, Def3;

          hence ((G1 '&' G2) . a) = (N . a) by A9, A17, A28, A32, Def3;

        end;

        hence ((G1 '&' G2) . a) = (N . a) by A4, A15, A17, A18, FINSEQ_1: 25;

      end;

      hence thesis by A15, FUNCT_1: 2;

    end;

    

     Lm2: F = (H / (x,y)) & (z = s & s <> x or z = y & s = x) implies ( All (z,F)) = (( All (s,H)) / (x,y))

    proof

      set N = (( All (s,H)) / (x,y));

      

       A1: ( len <*4*>) = 1 & (1 + 1) = 2 by FINSEQ_1: 39;

      ( len <*s*>) = 1 by FINSEQ_1: 39;

      then

       A2: ( len ( <*4*> ^ <*s*>)) = 2 by A1, FINSEQ_1: 22;

      then

       A3: ( dom ( <*4*> ^ <*s*>)) = {1, 2} by FINSEQ_1: 2, FINSEQ_1:def 3;

      ( len ( All (s,H))) = (2 + ( len H)) by A2, FINSEQ_1: 22;

      then

       A4: ( dom ( All (s,H))) = ( Seg (2 + ( len H))) by FINSEQ_1:def 3;

      

       A5: ( <*4*> ^ <*z*>) = <*4, z*> & ( <*4*> ^ <*s*>) = <*4, s*> by FINSEQ_1:def 9;

      

       A6: ( dom N) = ( dom ( All (s,H))) by Def3;

      assume that

       A7: F = (H / (x,y)) and

       A8: z = s & s <> x or z = y & s = x;

      

       A9: ( dom F) = ( dom H) by A7, Def3;

      ( len <*z*>) = 1 by FINSEQ_1: 39;

      then

       A10: ( len ( <*4*> ^ <*z*>)) = 2 by A1, FINSEQ_1: 22;

      then

       A11: ( dom ( <*4*> ^ <*z*>)) = {1, 2} by FINSEQ_1: 2, FINSEQ_1:def 3;

       A12:

      now

        let a be object;

        assume

         A13: a in ( dom N);

        then

        reconsider a1 = a as Element of NAT by A6;

         A14:

        now

          

           A15: x <> 4 & ( <*4, z*> . 1) = 4 by Th135, FINSEQ_1: 44;

          

           A16: ( <*4, s*> . 1) = 4 & ( <*4, z*> . 2) = z by FINSEQ_1: 44;

          

           A17: ( <*4, s*> . 2) = s by FINSEQ_1: 44;

          assume

           A18: a in {1, 2};

          then

           A19: a = 1 or a = 2 by TARSKI:def 2;

          (( All (z,F)) . a1) = ( <*4, z*> . a1) & (( All (s,H)) . a1) = ( <*4, s*> . a1) by A11, A3, A5, A18, FINSEQ_1:def 7;

          hence (( All (z,F)) . a) = ((( All (s,H)) / (x,y)) . a) by A8, A6, A13, A19, A15, A16, A17, Def3;

        end;

        now

          

           A20: (( All (s,H)) . a) <> x implies ((( All (s,H)) / (x,y)) . a) = (( All (s,H)) . a) by A6, A13, Def3;

          given i be Nat such that

           A21: i in ( dom H) and

           A22: a1 = (2 + i);

          

           A23: (( All (z,F)) . a) = (F . i) & (( All (s,H)) . a) = (H . i) by A10, A2, A9, A21, A22, FINSEQ_1:def 7;

          then

           A24: (( All (s,H)) . a) = x implies (( All (z,F)) . a) = y by A7, A21, Def3;

          (( All (s,H)) . a) <> x implies (( All (z,F)) . a) = (( All (s,H)) . a) by A7, A21, A23, Def3;

          hence (( All (z,F)) . a) = ((( All (s,H)) / (x,y)) . a) by A6, A13, A24, A20, Def3;

        end;

        hence (( All (z,F)) . a) = ((( All (s,H)) / (x,y)) . a) by A2, A3, A6, A13, A14, FINSEQ_1: 25;

      end;

      ( len ( All (z,F))) = (2 + ( len F)) by A10, FINSEQ_1: 22;

      then ( dom ( All (z,F))) = ( Seg (2 + ( len F))) by FINSEQ_1:def 3;

      then ( dom ( All (s,H))) = ( dom ( All (z,F))) by A4, A9, FINSEQ_3: 29;

      hence thesis by A6, A12, FUNCT_1: 2;

    end;

    theorem :: ZF_LANG1:157

    

     Th157: (H / (x,y)) in WFF

    proof

      defpred P[ ZF-formula] means ($1 / (x,y)) in WFF ;

      

       A1: for H st P[H] holds P[( 'not' H)]

      proof

        let H;

        assume (H / (x,y)) in WFF ;

        then

        reconsider F = (H / (x,y)) as ZF-formula by ZF_LANG: 4;

        ( 'not' F) = (( 'not' H) / (x,y)) by Th156;

        hence thesis by ZF_LANG: 4;

      end;

      

       A2: for H1, H2 st P[H1] & P[H2] holds P[(H1 '&' H2)]

      proof

        let H1, H2;

        assume (H1 / (x,y)) in WFF & (H2 / (x,y)) in WFF ;

        then

        reconsider F1 = (H1 / (x,y)), F2 = (H2 / (x,y)) as ZF-formula by ZF_LANG: 4;

        (F1 '&' F2) = ((H1 '&' H2) / (x,y)) by Lm1;

        hence thesis by ZF_LANG: 4;

      end;

      

       A3: for H, z st P[H] holds P[( All (z,H))]

      proof

        let H, z;

        assume (H / (x,y)) in WFF ;

        then

        reconsider F = (H / (x,y)) as ZF-formula by ZF_LANG: 4;

        z <> x or z = x;

        then

        consider s such that

         A4: s = z & z <> x or s = y & z = x;

        ( All (s,F)) = (( All (z,H)) / (x,y)) by A4, Lm2;

        hence thesis by ZF_LANG: 4;

      end;

      

       A5: for x1, x2 holds P[(x1 '=' x2)] & P[(x1 'in' x2)]

      proof

        let x1, x2;

        (ex y1, y2 st ((x1 '=' x2) / (x,y)) = (y1 '=' y2)) & ex z1, z2 st ((x1 'in' x2) / (x,y)) = (z1 'in' z2) by Th153, Th155;

        hence thesis by ZF_LANG: 4;

      end;

      for H holds P[H] from ZFInduction( A5, A1, A2, A3);

      hence thesis;

    end;

    definition

      let H, x, y;

      :: original: /

      redefine

      func H / (x,y) -> ZF-formula ;

      coherence by Th157, ZF_LANG: 4;

    end

    theorem :: ZF_LANG1:158

    

     Th158: (G1 '&' G2) = ((H1 '&' H2) / (x,y)) iff G1 = (H1 / (x,y)) & G2 = (H2 / (x,y))

    proof

      thus (G1 '&' G2) = ((H1 '&' H2) / (x,y)) implies G1 = (H1 / (x,y)) & G2 = (H2 / (x,y))

      proof

        assume (G1 '&' G2) = ((H1 '&' H2) / (x,y));

        then (G1 '&' G2) = ((H1 / (x,y)) '&' (H2 / (x,y))) by Lm1;

        hence thesis by ZF_LANG: 30;

      end;

      thus thesis by Lm1;

    end;

    theorem :: ZF_LANG1:159

    

     Th159: z <> x implies (( All (z,G)) = (( All (z,H)) / (x,y)) iff G = (H / (x,y)))

    proof

      assume

       A1: z <> x;

      thus ( All (z,G)) = (( All (z,H)) / (x,y)) implies G = (H / (x,y))

      proof

        assume ( All (z,G)) = (( All (z,H)) / (x,y));

        then ( All (z,G)) = ( All (z,(H / (x,y)))) by A1, Lm2;

        hence thesis by ZF_LANG: 3;

      end;

      thus thesis by A1, Lm2;

    end;

    theorem :: ZF_LANG1:160

    

     Th160: ( All (y,G)) = (( All (x,H)) / (x,y)) iff G = (H / (x,y))

    proof

      thus ( All (y,G)) = (( All (x,H)) / (x,y)) implies G = (H / (x,y))

      proof

        assume ( All (y,G)) = (( All (x,H)) / (x,y));

        then ( All (y,G)) = ( All (y,(H / (x,y)))) by Lm2;

        hence thesis by ZF_LANG: 3;

      end;

      thus thesis by Lm2;

    end;

    theorem :: ZF_LANG1:161

    

     Th161: (G1 'or' G2) = ((H1 'or' H2) / (x,y)) iff G1 = (H1 / (x,y)) & G2 = (H2 / (x,y))

    proof

      ( 'not' G1) = (( 'not' H1) / (x,y)) & ( 'not' G2) = (( 'not' H2) / (x,y)) iff (( 'not' G1) '&' ( 'not' G2)) = ((( 'not' H1) '&' ( 'not' H2)) / (x,y)) by Th158;

      hence thesis by Th156;

    end;

    theorem :: ZF_LANG1:162

    

     Th162: (G1 => G2) = ((H1 => H2) / (x,y)) iff G1 = (H1 / (x,y)) & G2 = (H2 / (x,y))

    proof

      G1 = (H1 / (x,y)) & ( 'not' G2) = (( 'not' H2) / (x,y)) iff (G1 '&' ( 'not' G2)) = ((H1 '&' ( 'not' H2)) / (x,y)) by Th158;

      hence thesis by Th156;

    end;

    theorem :: ZF_LANG1:163

    

     Th163: (G1 <=> G2) = ((H1 <=> H2) / (x,y)) iff G1 = (H1 / (x,y)) & G2 = (H2 / (x,y))

    proof

      (G1 <=> G2) = ((H1 <=> H2) / (x,y)) iff (G1 => G2) = ((H1 => H2) / (x,y)) & (G2 => G1) = ((H2 => H1) / (x,y)) by Th158;

      hence thesis by Th162;

    end;

    theorem :: ZF_LANG1:164

    

     Th164: z <> x implies (( Ex (z,G)) = (( Ex (z,H)) / (x,y)) iff G = (H / (x,y)))

    proof

      assume z <> x;

      then ( 'not' G) = (( 'not' H) / (x,y)) iff ( All (z,( 'not' G))) = (( All (z,( 'not' H))) / (x,y)) by Th159;

      hence thesis by Th156;

    end;

    theorem :: ZF_LANG1:165

    

     Th165: ( Ex (y,G)) = (( Ex (x,H)) / (x,y)) iff G = (H / (x,y))

    proof

      ( 'not' G) = (( 'not' H) / (x,y)) iff ( All (y,( 'not' G))) = (( All (x,( 'not' H))) / (x,y)) by Th160;

      hence thesis by Th156;

    end;

    theorem :: ZF_LANG1:166

    H is being_equality iff (H / (x,y)) is being_equality

    proof

      thus H is being_equality implies (H / (x,y)) is being_equality by Th153;

      assume (H / (x,y)) is being_equality;

      then

       A1: ((H / (x,y)) . 1) = 0 by ZF_LANG: 18;

      3 <= ( len H) by ZF_LANG: 13;

      then 1 <= ( len H) by XXREAL_0: 2;

      then

       A2: 1 in ( dom H) by FINSEQ_3: 25;

      y <> 0 by Th135;

      then (H . 1) <> x by A1, A2, Def3;

      then 0 = (H . 1) by A1, A2, Def3;

      hence thesis by ZF_LANG: 24;

    end;

    theorem :: ZF_LANG1:167

    H is being_membership iff (H / (x,y)) is being_membership

    proof

      thus H is being_membership implies (H / (x,y)) is being_membership by Th155;

      assume (H / (x,y)) is being_membership;

      then

       A1: ((H / (x,y)) . 1) = 1 by ZF_LANG: 19;

      3 <= ( len H) by ZF_LANG: 13;

      then 1 <= ( len H) by XXREAL_0: 2;

      then

       A2: 1 in ( dom H) by FINSEQ_3: 25;

      y <> 1 by Th135;

      then (H . 1) <> x by A1, A2, Def3;

      then 1 = (H . 1) by A1, A2, Def3;

      hence thesis by ZF_LANG: 25;

    end;

    theorem :: ZF_LANG1:168

    

     Th168: H is negative iff (H / (x,y)) is negative

    proof

      thus H is negative implies (H / (x,y)) is negative

      proof

        given H1 such that

         A1: H = ( 'not' H1);

        (H / (x,y)) = ( 'not' (H1 / (x,y))) by A1, Th156;

        hence thesis;

      end;

      assume (H / (x,y)) is negative;

      then

       A2: ((H / (x,y)) . 1) = 2 by ZF_LANG: 20;

      3 <= ( len H) by ZF_LANG: 13;

      then 1 <= ( len H) by XXREAL_0: 2;

      then

       A3: 1 in ( dom H) by FINSEQ_3: 25;

      y <> 2 by Th135;

      then (H . 1) <> x by A2, A3, Def3;

      then 2 = (H . 1) by A2, A3, Def3;

      hence thesis by ZF_LANG: 26;

    end;

    theorem :: ZF_LANG1:169

    

     Th169: H is conjunctive iff (H / (x,y)) is conjunctive

    proof

      thus H is conjunctive implies (H / (x,y)) is conjunctive

      proof

        given H1, H2 such that

         A1: H = (H1 '&' H2);

        (H / (x,y)) = ((H1 / (x,y)) '&' (H2 / (x,y))) by A1, Th158;

        hence thesis;

      end;

      assume (H / (x,y)) is conjunctive;

      then

       A2: ((H / (x,y)) . 1) = 3 by ZF_LANG: 21;

      3 <= ( len H) by ZF_LANG: 13;

      then 1 <= ( len H) by XXREAL_0: 2;

      then

       A3: 1 in ( dom H) by FINSEQ_3: 25;

      y <> 3 by Th135;

      then (H . 1) <> x by A2, A3, Def3;

      then 3 = (H . 1) by A2, A3, Def3;

      hence thesis by ZF_LANG: 27;

    end;

    theorem :: ZF_LANG1:170

    

     Th170: H is universal iff (H / (x,y)) is universal

    proof

      thus H is universal implies (H / (x,y)) is universal

      proof

        given z, H1 such that

         A1: H = ( All (z,H1));

        z = x or z <> x;

        then

        consider s such that

         A2: z = x & s = y or z <> x & s = z;

        (H / (x,y)) = ( All (s,(H1 / (x,y)))) by A1, A2, Th159, Th160;

        hence thesis;

      end;

      assume (H / (x,y)) is universal;

      then

       A3: ((H / (x,y)) . 1) = 4 by ZF_LANG: 22;

      3 <= ( len H) by ZF_LANG: 13;

      then 1 <= ( len H) by XXREAL_0: 2;

      then

       A4: 1 in ( dom H) by FINSEQ_3: 25;

      y <> 4 by Th135;

      then (H . 1) <> x by A3, A4, Def3;

      then 4 = (H . 1) by A3, A4, Def3;

      hence thesis by ZF_LANG: 28;

    end;

    theorem :: ZF_LANG1:171

    H is negative implies ( the_argument_of (H / (x,y))) = (( the_argument_of H) / (x,y))

    proof

      assume

       A1: H is negative;

      then (H / (x,y)) is negative by Th168;

      then

       A2: (H / (x,y)) = ( 'not' ( the_argument_of (H / (x,y)))) by ZF_LANG:def 30;

      H = ( 'not' ( the_argument_of H)) by A1, ZF_LANG:def 30;

      hence thesis by A2, Th156;

    end;

    theorem :: ZF_LANG1:172

    H is conjunctive implies ( the_left_argument_of (H / (x,y))) = (( the_left_argument_of H) / (x,y)) & ( the_right_argument_of (H / (x,y))) = (( the_right_argument_of H) / (x,y))

    proof

      assume

       A1: H is conjunctive;

      then (H / (x,y)) is conjunctive by Th169;

      then

       A2: (H / (x,y)) = (( the_left_argument_of (H / (x,y))) '&' ( the_right_argument_of (H / (x,y)))) by ZF_LANG: 40;

      H = (( the_left_argument_of H) '&' ( the_right_argument_of H)) by A1, ZF_LANG: 40;

      hence thesis by A2, Th158;

    end;

    theorem :: ZF_LANG1:173

    H is universal implies ( the_scope_of (H / (x,y))) = (( the_scope_of H) / (x,y)) & (( bound_in H) = x implies ( bound_in (H / (x,y))) = y) & (( bound_in H) <> x implies ( bound_in (H / (x,y))) = ( bound_in H))

    proof

      assume

       A1: H is universal;

      then (H / (x,y)) is universal by Th170;

      then

       A2: (H / (x,y)) = ( All (( bound_in (H / (x,y))),( the_scope_of (H / (x,y))))) by ZF_LANG: 44;

      

       A3: H = ( All (( bound_in H),( the_scope_of H))) by A1, ZF_LANG: 44;

      then

       A4: ( bound_in H) <> x implies (H / (x,y)) = ( All (( bound_in H),(( the_scope_of H) / (x,y)))) by Th159;

      ( bound_in H) = x implies (H / (x,y)) = ( All (y,(( the_scope_of H) / (x,y)))) by A3, Th160;

      hence thesis by A2, A4, ZF_LANG: 3;

    end;

    theorem :: ZF_LANG1:174

    

     Th174: H is disjunctive iff (H / (x,y)) is disjunctive

    proof

      set G = (H / (x,y));

      thus H is disjunctive implies (H / (x,y)) is disjunctive

      proof

        given H1, H2 such that

         A1: H = (H1 'or' H2);

        (H / (x,y)) = ((H1 / (x,y)) 'or' (H2 / (x,y))) by A1, Th161;

        hence thesis;

      end;

      given G1, G2 such that

       A2: G = (G1 'or' G2);

      G is negative by A2;

      then H is negative by Th168;

      then

      consider H9 be ZF-formula such that

       A3: H = ( 'not' H9);

      

       A4: (( 'not' G1) '&' ( 'not' G2)) = (H9 / (x,y)) by A2, A3, Th156;

      then (H9 / (x,y)) is conjunctive;

      then H9 is conjunctive by Th169;

      then

      consider H1, H2 such that

       A5: H9 = (H1 '&' H2);

      ( 'not' G2) = (H2 / (x,y)) by A4, A5, Th158;

      then (H2 / (x,y)) is negative;

      then H2 is negative by Th168;

      then

      consider p2 such that

       A6: H2 = ( 'not' p2);

      ( 'not' G1) = (H1 / (x,y)) by A4, A5, Th158;

      then (H1 / (x,y)) is negative;

      then H1 is negative by Th168;

      then

      consider p1 such that

       A7: H1 = ( 'not' p1);

      H = (p1 'or' p2) by A3, A5, A7, A6;

      hence thesis;

    end;

    theorem :: ZF_LANG1:175

    

     Th175: H is conditional iff (H / (x,y)) is conditional

    proof

      set G = (H / (x,y));

      thus H is conditional implies (H / (x,y)) is conditional

      proof

        given H1, H2 such that

         A1: H = (H1 => H2);

        (H / (x,y)) = ((H1 / (x,y)) => (H2 / (x,y))) by A1, Th162;

        hence thesis;

      end;

      given G1, G2 such that

       A2: G = (G1 => G2);

      G is negative by A2;

      then H is negative by Th168;

      then

      consider H9 be ZF-formula such that

       A3: H = ( 'not' H9);

      

       A4: (G1 '&' ( 'not' G2)) = (H9 / (x,y)) by A2, A3, Th156;

      then (H9 / (x,y)) is conjunctive;

      then H9 is conjunctive by Th169;

      then

      consider H1, H2 such that

       A5: H9 = (H1 '&' H2);

      ( 'not' G2) = (H2 / (x,y)) by A4, A5, Th158;

      then (H2 / (x,y)) is negative;

      then H2 is negative by Th168;

      then

      consider p2 such that

       A6: H2 = ( 'not' p2);

      H = (H1 => p2) by A3, A5, A6;

      hence thesis;

    end;

    theorem :: ZF_LANG1:176

    

     Th176: H is biconditional implies (H / (x,y)) is biconditional

    proof

      given H1, H2 such that

       A1: H = (H1 <=> H2);

      (H / (x,y)) = ((H1 / (x,y)) <=> (H2 / (x,y))) by A1, Th163;

      hence thesis;

    end;

    theorem :: ZF_LANG1:177

    

     Th177: H is existential iff (H / (x,y)) is existential

    proof

      thus H is existential implies (H / (x,y)) is existential

      proof

        given z, H1 such that

         A1: H = ( Ex (z,H1));

        z = x or z <> x;

        then

        consider s such that

         A2: z = x & s = y or z <> x & s = z;

        (H / (x,y)) = ( Ex (s,(H1 / (x,y)))) by A1, A2, Th164, Th165;

        hence thesis;

      end;

      given z, G such that

       A3: (H / (x,y)) = ( Ex (z,G));

      (H / (x,y)) is negative by A3;

      then H is negative by Th168;

      then

      consider H1 such that

       A4: H = ( 'not' H1);

      ( bound_in H1) = x or ( bound_in H1) <> x;

      then

      consider s such that

       A5: ( bound_in H1) = x & s = y or ( bound_in H1) <> x & s = ( bound_in H1);

      

       A6: (H1 / (x,y)) = ( All (z,( 'not' G))) by A3, A4, Th156;

      then (H1 / (x,y)) is universal;

      then H1 is universal by Th170;

      then

       A7: H1 = ( All (( bound_in H1),( the_scope_of H1))) by ZF_LANG: 44;

      then ( All (z,( 'not' G))) = ( All (s,(( the_scope_of H1) / (x,y)))) by A6, A5, Th159, Th160;

      then ( 'not' G) = (( the_scope_of H1) / (x,y)) by ZF_LANG: 3;

      then (( the_scope_of H1) / (x,y)) is negative;

      then ( the_scope_of H1) is negative by Th168;

      then H = ( Ex (( bound_in H1),( the_argument_of ( the_scope_of H1)))) by A4, A7, ZF_LANG:def 30;

      hence thesis;

    end;

    theorem :: ZF_LANG1:178

    H is disjunctive implies ( the_left_argument_of (H / (x,y))) = (( the_left_argument_of H) / (x,y)) & ( the_right_argument_of (H / (x,y))) = (( the_right_argument_of H) / (x,y))

    proof

      assume

       A1: H is disjunctive;

      then (H / (x,y)) is disjunctive by Th174;

      then

       A2: (H / (x,y)) = (( the_left_argument_of (H / (x,y))) 'or' ( the_right_argument_of (H / (x,y)))) by ZF_LANG: 41;

      H = (( the_left_argument_of H) 'or' ( the_right_argument_of H)) by A1, ZF_LANG: 41;

      hence thesis by A2, Th161;

    end;

    theorem :: ZF_LANG1:179

    H is conditional implies ( the_antecedent_of (H / (x,y))) = (( the_antecedent_of H) / (x,y)) & ( the_consequent_of (H / (x,y))) = (( the_consequent_of H) / (x,y))

    proof

      assume

       A1: H is conditional;

      then (H / (x,y)) is conditional by Th175;

      then

       A2: (H / (x,y)) = (( the_antecedent_of (H / (x,y))) => ( the_consequent_of (H / (x,y)))) by ZF_LANG: 47;

      H = (( the_antecedent_of H) => ( the_consequent_of H)) by A1, ZF_LANG: 47;

      hence thesis by A2, Th162;

    end;

    theorem :: ZF_LANG1:180

    H is biconditional implies ( the_left_side_of (H / (x,y))) = (( the_left_side_of H) / (x,y)) & ( the_right_side_of (H / (x,y))) = (( the_right_side_of H) / (x,y))

    proof

      assume H is biconditional;

      then H = (( the_left_side_of H) <=> ( the_right_side_of H)) & (H / (x,y)) = (( the_left_side_of (H / (x,y))) <=> ( the_right_side_of (H / (x,y)))) by Th176, ZF_LANG: 49;

      hence thesis by Th163;

    end;

    theorem :: ZF_LANG1:181

    H is existential implies ( the_scope_of (H / (x,y))) = (( the_scope_of H) / (x,y)) & (( bound_in H) = x implies ( bound_in (H / (x,y))) = y) & (( bound_in H) <> x implies ( bound_in (H / (x,y))) = ( bound_in H))

    proof

      assume

       A1: H is existential;

      then (H / (x,y)) is existential by Th177;

      then

       A2: (H / (x,y)) = ( Ex (( bound_in (H / (x,y))),( the_scope_of (H / (x,y))))) by ZF_LANG: 45;

      

       A3: H = ( Ex (( bound_in H),( the_scope_of H))) by A1, ZF_LANG: 45;

      then

       A4: ( bound_in H) <> x implies (H / (x,y)) = ( Ex (( bound_in H),(( the_scope_of H) / (x,y)))) by Th164;

      ( bound_in H) = x implies (H / (x,y)) = ( Ex (y,(( the_scope_of H) / (x,y)))) by A3, Th165;

      hence thesis by A2, A4, ZF_LANG: 34;

    end;

    theorem :: ZF_LANG1:182

    

     Th182: not x in ( variables_in H) implies (H / (x,y)) = H

    proof

      assume

       A1: not x in ( variables_in H);

      

       A2: not x in { 0 , 1, 2, 3, 4} by Th136;

       A3:

      now

        let a be object;

        assume

         A4: a in ( dom H);

        then

         A5: (H . a) in ( rng H) by FUNCT_1:def 3;

        (H . a) <> x implies ((H / (x,y)) . a) = (H . a) by A4, Def3;

        hence ((H / (x,y)) . a) = (H . a) by A1, A2, A5, XBOOLE_0:def 5;

      end;

      ( dom H) = ( dom (H / (x,y))) by Def3;

      hence thesis by A3, FUNCT_1: 2;

    end;

    theorem :: ZF_LANG1:183

    (H / (x,x)) = H

    proof

       A1:

      now

        let a be object;

        assume

         A2: a in ( dom H);

        then (H . a) = x implies ((H / (x,x)) . a) = x by Def3;

        hence (H . a) = ((H / (x,x)) . a) by A2, Def3;

      end;

      ( dom (H / (x,x))) = ( dom H) by Def3;

      hence thesis by A1, FUNCT_1: 2;

    end;

    theorem :: ZF_LANG1:184

    

     Th184: x <> y implies not x in ( variables_in (H / (x,y)))

    proof

      assume

       A1: x <> y;

      assume x in ( variables_in (H / (x,y)));

      then

      consider a be object such that

       A2: a in ( dom (H / (x,y))) and

       A3: x = ((H / (x,y)) . a) by FUNCT_1:def 3;

      

       A4: ( dom (H / (x,y))) = ( dom H) by Def3;

      then (H . a) = x implies ((H / (x,y)) . a) = y by A2, Def3;

      hence contradiction by A1, A2, A3, A4, Def3;

    end;

    theorem :: ZF_LANG1:185

    x in ( variables_in H) implies y in ( variables_in (H / (x,y)))

    proof

      assume x in ( variables_in H);

      then

      consider a be object such that

       A1: a in ( dom H) and

       A2: x = (H . a) by FUNCT_1:def 3;

      

       A3: ( dom (H / (x,y))) = ( dom H) by Def3;

      

       A4: not y in { 0 , 1, 2, 3, 4} by Th136;

      ((H / (x,y)) . a) = y by A1, A2, Def3;

      then y in ( rng (H / (x,y))) by A1, A3, FUNCT_1:def 3;

      hence thesis by A4, XBOOLE_0:def 5;

    end;

    theorem :: ZF_LANG1:186

    x <> y implies ((H / (x,y)) / (x,z)) = (H / (x,y))

    proof

      assume x <> y;

      then not x in ( variables_in (H / (x,y))) by Th184;

      hence thesis by Th182;

    end;

    theorem :: ZF_LANG1:187

    ( variables_in (H / (x,y))) c= ((( variables_in H) \ {x}) \/ {y})

    proof

      let a be object;

      assume

       A1: a in ( variables_in (H / (x,y)));

      then

      reconsider z = a as Variable;

      consider b be object such that

       A2: b in ( dom (H / (x,y))) and

       A3: z = ((H / (x,y)) . b) by A1, FUNCT_1:def 3;

      

       A4: ( dom (H / (x,y))) = ( dom H) by Def3;

      then

       A5: (H . b) <> x implies z = (H . b) by A2, A3, Def3;

      (H . b) = x implies z = y by A2, A3, A4, Def3;

      then z in {y} or z in ( rng H) & not z in { 0 , 1, 2, 3, 4} & not z in {x} by A2, A4, A5, Th136, FUNCT_1:def 3, TARSKI:def 1;

      then z in {y} or z in (( rng H) \ { 0 , 1, 2, 3, 4}) & not z in {x} by XBOOLE_0:def 5;

      then z in {y} or z in (( variables_in H) \ {x}) by XBOOLE_0:def 5;

      hence thesis by XBOOLE_0:def 3;

    end;