let A be set ; :: thesis: for a being Element of DISJOINT_PAIRS A
for K being Element of Normal_forms_on A st K ^ {a} = {} holds
ex b being Element of DISJOINT_PAIRS A st
( b in - K & b c= a )
let a be Element of DISJOINT_PAIRS A; :: thesis: for K being Element of Normal_forms_on A st K ^ {a} = {} holds
ex b being Element of DISJOINT_PAIRS A st
( b in - K & b c= a )
let K be Element of Normal_forms_on A; :: thesis: ( K ^ {a} = {} implies ex b being Element of DISJOINT_PAIRS A st
( b in - K & b c= a ) )
assume A1: K ^ {a} = {} ; :: thesis: ex b being Element of DISJOINT_PAIRS A st
( b in - K & b c= a )

now

per cases ( not A is empty or A is empty ) ;

suppose not A is empty ; :: thesis: ex c being Element of DISJOINT_PAIRS A st
( c in - K & c c= a )

then A2: A = [A] by Def2;
defpred S₁[ set , set ] means $2 in (($1 `1 ) /\ (a `2 )) \/ (($1 `2 ) /\ (a `1 ));

A3: now

let s be Element of DISJOINT_PAIRS A; :: thesis: ( s in K implies ex x being Element of [A] st S₁[s,x] )
assume A4: s in K ; :: thesis: ex x being Element of [A] st S₁[s,x]
a in {a} by TARSKI:def 1;
then not s \/ a in DISJOINT_PAIRS A by A1, A4, NORMFORM:56;
then consider x being Element of [A] such that
A5: ( ( x in s `1 & x in a `2 ) or ( x in a `1 & x in s `2 ) ) by A2, NORMFORM:47;
take x = x; :: thesis: S₁[s,x]
( x in (s `1 ) /\ (a `2 ) or x in (s `2 ) /\ (a `1 ) ) by A5, XBOOLE_0:def 4;
hence S₁[s,x] by XBOOLE_0:def 3; :: thesis: verum

end;

consider g being Element of Funcs (DISJOINT_PAIRS A),[A] such that
A6: for s being Element of DISJOINT_PAIRS A st s in K holds
S₁[s,g . s] from FRAENKEL:sch 27(A3);

A7: now

let s be Element of DISJOINT_PAIRS A; :: thesis: ( s in K implies g . s in (s `1 ) \/ (s `2 ) )
assume s in K ; :: thesis: g . s in (s `1 ) \/ (s `2 )
then g . s in ((s `1 ) /\ (a `2 )) \/ ((s `2 ) /\ (a `1 )) by A6;
then ( g . s in (s `1 ) /\ (a `2 ) or g . s in (s `2 ) /\ (a `1 ) ) by XBOOLE_0:def 3;
then ( ( g . s in s `1 & g . s in a `2 ) or ( g . s in s `2 & g . s in a `1 ) ) by XBOOLE_0:def 4;
hence g . s in (s `1 ) \/ (s `2 ) by XBOOLE_0:def 3; :: thesis: verum

end;

set c1 = { (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in K ) } ;
set c2 = { (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in K ) } ;
A8: { (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in K ) } c= a `1

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in K ) } or x in a `1 )
assume x in { (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in K ) } ; :: thesis: x in a `1
then consider t being Element of DISJOINT_PAIRS A such that
A9: ( x = g . t & g . t in t `2 ) and
A10: t in K ;
g . t in ((t `1 ) /\ (a `2 )) \/ ((t `2 ) /\ (a `1 )) by A6, A10;
then ( g . t in (t `1 ) /\ (a `2 ) or g . t in (t `2 ) /\ (a `1 ) ) by XBOOLE_0:def 3;
then ( ( g . t in t `1 & g . t in a `2 ) or ( g . t in t `2 & g . t in a `1 ) ) by XBOOLE_0:def 4;
hence x in a `1 by A9, NORMFORM:46; :: thesis: verum

end;

A11: { (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in K ) } c= a `2

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in K ) } or x in a `2 )
assume x in { (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in K ) } ; :: thesis: x in a `2
then consider t being Element of DISJOINT_PAIRS A such that
A12: ( x = g . t & g . t in t `1 ) and
A13: t in K ;
g . t in ((t `1 ) /\ (a `2 )) \/ ((t `2 ) /\ (a `1 )) by A6, A13;
then ( g . t in (t `1 ) /\ (a `2 ) or g . t in (t `2 ) /\ (a `1 ) ) by XBOOLE_0:def 3;
then ( ( g . t in t `1 & g . t in a `2 ) or ( g . t in t `2 & g . t in a `1 ) ) by XBOOLE_0:def 4;
hence x in a `2 by A12, NORMFORM:46; :: thesis: verum

end;

then reconsider c = [{ (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in K ) } ,{ (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in K ) } ] as Element of DISJOINT_PAIRS A by A8, NORMFORM:50;
take c = c; :: thesis: ( c in - K & c c= a )
c in { [{ (h . t1) where t1 is Element of DISJOINT_PAIRS A : ( h . t1 in t1 `2 & t1 in K ) } ,{ (h . t2) where t2 is Element of DISJOINT_PAIRS A : ( h . t2 in t2 `1 & t2 in K ) } ] where h is Element of Funcs (DISJOINT_PAIRS A),[A] : for s being Element of DISJOINT_PAIRS A st s in K holds
h . s in (s `1 ) \/ (s `2 ) } by A7;
hence c in - K by XBOOLE_0:def 4; :: thesis: c c= a
( c `1 = { (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in K ) } & c `2 = { (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in K ) } ) by MCART_1:7;
hence c c= a by A8, A11, NORMFORM:def 1; :: thesis: verum

end;

suppose A14: A is empty ; :: thesis: ex b being Element of DISJOINT_PAIRS A st
( b in - K & b c= a )

then A15: a = [{} ,{} ] by Th20;
take b = a; :: thesis: ( b in - K & b c= a )
reconsider Z = {[{} ,{} ]} as Element of Normal_forms_on {} by Th22;
mi (Z ^ Z) <> {} by Th7;
then K <> {[{} ,{} ]} by A1, A14, A15, NORMFORM:64, XBOOLE_1:3;
then K = {} by A14, Lm4, TARSKI:def 2;
then - K = {[{} ,{} ]} by Th18;
hence b in - K by A15, TARSKI:def 1; :: thesis: b c= a
thus b c= a ; :: thesis: verum

end;

end;

end;

hence ex b being Element of DISJOINT_PAIRS A st
( b in - K & b c= a ) ; :: thesis: verum