let A be set ; :: thesis: for a being Element of DISJOINT_PAIRS A
for u being Element of (NormForm A) ex v being Element of (NormForm A) st
( v in SUB u & (@ v) ^ {a} = {} & ( for b being Element of DISJOINT_PAIRS A st b in (diff u) . v holds
b \/ a in DISJOINT_PAIRS A ) )
let a be Element of DISJOINT_PAIRS A; :: thesis: for u being Element of (NormForm A) ex v being Element of (NormForm A) st
( v in SUB u & (@ v) ^ {a} = {} & ( for b being Element of DISJOINT_PAIRS A st b in (diff u) . v holds
b \/ a in DISJOINT_PAIRS A ) )
let u be Element of (NormForm A); :: thesis: ex v being Element of (NormForm A) st
( v in SUB u & (@ v) ^ {a} = {} & ( for b being Element of DISJOINT_PAIRS A st b in (diff u) . v holds
b \/ a in DISJOINT_PAIRS A ) )
defpred S₁[ set ] means verum;
deffunc H₃( set ) -> set = $1;
defpred S₂[ Element of DISJOINT_PAIRS A] means not $1 \/ a in DISJOINT_PAIRS A;
set M = { H₃(s) where s is Element of DISJOINT_PAIRS A : ( H₃(s) in u & S₂[s] ) } ;
deffunc H₄( Element of DISJOINT_PAIRS A) -> Element of [:(Fin A),(Fin A):] = $1 \/ a;
defpred S₃[ set ] means $1 in u;
defpred S₄[ Element of DISJOINT_PAIRS A] means ( S₃[$1] & S₂[$1] );
A1: { H₄(t) where t is Element of DISJOINT_PAIRS A : ( t in { s where s is Element of DISJOINT_PAIRS A : S₄[s] } & S₁[t] ) } = { H₄(s) where s is Element of DISJOINT_PAIRS A : ( S₄[s] & S₁[s] ) } from FRAENKEL:sch 14();
defpred S₅[ set , set ] means $1 in { H₃(s) where s is Element of DISJOINT_PAIRS A : ( H₃(s) in u & S₂[s] ) } ;
defpred S₆[ set , set ] means ( $1 in { H₃(s) where s is Element of DISJOINT_PAIRS A : ( H₃(s) in u & S₂[s] ) } & $2 in {a} );
A2: { H₄(s1) where s1 is Element of DISJOINT_PAIRS A : ( S₄[s1] & S₁[s1] ) } = { H₄(s2) where s2 is Element of DISJOINT_PAIRS A : S₄[s2] }

proof

thus { H₄(s1) where s1 is Element of DISJOINT_PAIRS A : ( S₄[s1] & S₁[s1] ) } c= { H₄(s2) where s2 is Element of DISJOINT_PAIRS A : S₄[s2] } :: according to XBOOLE_0:def 10 :: thesis: { H₄(s2) where s2 is Element of DISJOINT_PAIRS A : S₄[s2] } c= { H₄(s1) where s1 is Element of DISJOINT_PAIRS A : ( S₄[s1] & S₁[s1] ) }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { H₄(s1) where s1 is Element of DISJOINT_PAIRS A : ( S₄[s1] & S₁[s1] ) } or x in { H₄(s2) where s2 is Element of DISJOINT_PAIRS A : S₄[s2] } )
assume x in { H₄(s1) where s1 is Element of DISJOINT_PAIRS A : ( S₄[s1] & S₁[s1] ) } ; :: thesis: x in { H₄(s2) where s2 is Element of DISJOINT_PAIRS A : S₄[s2] }
then ex s1 being Element of DISJOINT_PAIRS A st
( x = H₄(s1) & S₄[s1] & S₁[s1] ) ;
hence x in { H₄(s2) where s2 is Element of DISJOINT_PAIRS A : S₄[s2] } ; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { H₄(s2) where s2 is Element of DISJOINT_PAIRS A : S₄[s2] } or x in { H₄(s1) where s1 is Element of DISJOINT_PAIRS A : ( S₄[s1] & S₁[s1] ) } )
assume x in { H₄(s1) where s1 is Element of DISJOINT_PAIRS A : S₄[s1] } ; :: thesis: x in { H₄(s1) where s1 is Element of DISJOINT_PAIRS A : ( S₄[s1] & S₁[s1] ) }
then ex s1 being Element of DISJOINT_PAIRS A st
( x = H₄(s1) & S₄[s1] ) ;
hence x in { H₄(s1) where s1 is Element of DISJOINT_PAIRS A : ( S₄[s1] & S₁[s1] ) } ; :: thesis: verum

end;

A3: { H₃(s) where s is Element of DISJOINT_PAIRS A : ( H₃(s) in u & S₂[s] ) } c= u from FRAENKEL:sch 17();
then reconsider v = { H₃(s) where s is Element of DISJOINT_PAIRS A : ( H₃(s) in u & S₂[s] ) } as Element of (NormForm A) by Th5;
take v ; :: thesis: ( v in SUB u & (@ v) ^ {a} = {} & ( for b being Element of DISJOINT_PAIRS A st b in (diff u) . v holds
b \/ a in DISJOINT_PAIRS A ) )
thus v in SUB u by A3; :: thesis: ( (@ v) ^ {a} = {} & ( for b being Element of DISJOINT_PAIRS A st b in (diff u) . v holds
b \/ a in DISJOINT_PAIRS A ) )
defpred S₇[ set , set ] means ( $2 = a & $1 in { H₃(s) where s is Element of DISJOINT_PAIRS A : ( H₃(s) in u & S₂[s] ) } );
deffunc H₅( Element of DISJOINT_PAIRS A, Element of DISJOINT_PAIRS A) -> Element of [:(Fin A),(Fin A):] = $1 \/ $2;
A4: { H₄(t) where t is Element of DISJOINT_PAIRS A : ( t in { s where s is Element of DISJOINT_PAIRS A : S₄[s] } & S₁[t] ) } = { H₄(t1) where t1 is Element of DISJOINT_PAIRS A : t1 in { s1 where s1 is Element of DISJOINT_PAIRS A : S₄[s1] } }

proof

thus { H₄(t) where t is Element of DISJOINT_PAIRS A : ( t in { s where s is Element of DISJOINT_PAIRS A : S₄[s] } & S₁[t] ) } c= { H₄(t1) where t1 is Element of DISJOINT_PAIRS A : t1 in { s1 where s1 is Element of DISJOINT_PAIRS A : S₄[s1] } } :: according to XBOOLE_0:def 10 :: thesis: { H₄(t1) where t1 is Element of DISJOINT_PAIRS A : t1 in { s1 where s1 is Element of DISJOINT_PAIRS A : S₄[s1] } } c= { H₄(t) where t is Element of DISJOINT_PAIRS A : ( t in { s where s is Element of DISJOINT_PAIRS A : S₄[s] } & S₁[t] ) }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { H₄(t) where t is Element of DISJOINT_PAIRS A : ( t in { s where s is Element of DISJOINT_PAIRS A : S₄[s] } & S₁[t] ) } or x in { H₄(t1) where t1 is Element of DISJOINT_PAIRS A : t1 in { s1 where s1 is Element of DISJOINT_PAIRS A : S₄[s1] } } )
assume x in { H₄(t) where t is Element of DISJOINT_PAIRS A : ( t in { s where s is Element of DISJOINT_PAIRS A : S₄[s] } & S₁[t] ) } ; :: thesis: x in { H₄(t1) where t1 is Element of DISJOINT_PAIRS A : t1 in { s1 where s1 is Element of DISJOINT_PAIRS A : S₄[s1] } }
then ex t being Element of DISJOINT_PAIRS A st
( x = H₄(t) & t in { s where s is Element of DISJOINT_PAIRS A : S₄[s] } & S₁[t] ) ;
hence x in { H₄(t1) where t1 is Element of DISJOINT_PAIRS A : t1 in { s1 where s1 is Element of DISJOINT_PAIRS A : S₄[s1] } } ; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { H₄(t1) where t1 is Element of DISJOINT_PAIRS A : t1 in { s1 where s1 is Element of DISJOINT_PAIRS A : S₄[s1] } } or x in { H₄(t) where t is Element of DISJOINT_PAIRS A : ( t in { s where s is Element of DISJOINT_PAIRS A : S₄[s] } & S₁[t] ) } )
assume x in { H₄(t) where t is Element of DISJOINT_PAIRS A : t in { s where s is Element of DISJOINT_PAIRS A : S₄[s] } } ; :: thesis: x in { H₄(t) where t is Element of DISJOINT_PAIRS A : ( t in { s where s is Element of DISJOINT_PAIRS A : S₄[s] } & S₁[t] ) }
then ex t being Element of DISJOINT_PAIRS A st
( x = H₄(t) & t in { s where s is Element of DISJOINT_PAIRS A : S₄[s] } ) ;
hence x in { H₄(t) where t is Element of DISJOINT_PAIRS A : ( t in { s where s is Element of DISJOINT_PAIRS A : S₄[s] } & S₁[t] ) } ; :: thesis: verum

end;

A5: { H₅(s,t) where s, t is Element of DISJOINT_PAIRS A : ( t = a & S₅[s,t] ) } = { H₅(s9,a) where s9 is Element of DISJOINT_PAIRS A : S₅[s9,a] } from FRAENKEL:sch 20();
A6: for s, t being Element of DISJOINT_PAIRS A holds
( S₆[s,t] iff S₇[s,t] ) by TARSKI:def 1;
A7: { H₅(s,t) where s, t is Element of DISJOINT_PAIRS A : S₆[s,t] } = { H₅(s9,t9) where s9, t9 is Element of DISJOINT_PAIRS A : S₇[s9,t9] } from FRAENKEL:sch 4(A6);
{ H₄(s) where s is Element of DISJOINT_PAIRS A : ( S₃[s] & not H₄(s) in DISJOINT_PAIRS A ) } misses DISJOINT_PAIRS A from FRAENKEL:sch 18();
hence (@ v) ^ {a} = {} by A1, A4, A2, A7, A5; :: thesis: for b being Element of DISJOINT_PAIRS A st b in (diff u) . v holds
b \/ a in DISJOINT_PAIRS A
let b be Element of DISJOINT_PAIRS A; :: thesis: ( b in (diff u) . v implies b \/ a in DISJOINT_PAIRS A )
assume b in (diff u) . v ; :: thesis: b \/ a in DISJOINT_PAIRS A
then A8: b in u \ v by Def11;
then not b in { H₃(s) where s is Element of DISJOINT_PAIRS A : ( H₃(s) in u & S₂[s] ) } by XBOOLE_0:def 5;
hence b \/ a in DISJOINT_PAIRS A by A8; :: thesis: verum