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 :: thesis: ex c being Element of DISJOINT_PAIRS A st
( c in - K & c c= a )

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

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

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

A4: now :: thesis: for s being Element of DISJOINT_PAIRS A st s in K holds
ex x being Element of [A] st S₁[s,x]

A5: a in {a} by TARSKI:def 1;
let s be Element of DISJOINT_PAIRS A; :: thesis: ( s in K implies ex x being Element of [A] st S₁[s,x] )
assume s in K ; :: thesis: ex x being Element of [A] st S₁[s,x]
then not s \/ a in DISJOINT_PAIRS A by A1, A5, NORMFORM:35;
then consider x being Element of [A] such that
A6: ( ( x in s `1 & x in a `2 ) or ( x in a `1 & x in s `2 ) ) by A3, NORMFORM:28;
take x = x; :: thesis: S₁[s,x]
( x in (s `1) /\ (a `2) or x in (s `2) /\ (a `1) ) by A6, 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
A7: for s being Element of DISJOINT_PAIRS A st s in K holds
S₁[s,g . s] from FRAENKEL:sch 27(A4);
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 . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in K ) } c= a `2

proof

let x be object ; :: 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
A9: ( x = g . t & g . t in t `1 ) and
A10: t in K ;
g . t in ((t `1) /\ (a `2)) \/ ((t `2) /\ (a `1)) by A7, 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 `2 by A9, NORMFORM:27; :: thesis: verum

end;

A11: { (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 object ; :: 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
A12: ( x = g . t & g . t in t `2 ) and
A13: t in K ;
g . t in ((t `1) /\ (a `2)) \/ ((t `2) /\ (a `1)) by A7, 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 `1 by A12, NORMFORM:27; :: 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:30;
take c = c; :: thesis: ( c in - K & c c= a )

now :: thesis: for s being Element of DISJOINT_PAIRS A st s in K holds
g . s in (s `1) \/ (s `2)

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 A7;
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;

then 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) } ;
hence c in - K by XBOOLE_0:def 4; :: thesis: c c= a
thus c c= a by A11, A8; :: thesis: verum

end;

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

reconsider Z = {[{},{}]} as Element of Normal_forms_on {} by Th17;
take b = a; :: thesis: ( b in - K & b c= a )
A15: a = [{},{}] by A14, Th15;
mi (Z ^ Z) <> {} by Th3;
then K <> {[{},{}]} by A1, A14, A15, NORMFORM:40, XBOOLE_1:3;
then K = {} by A14, Lm4, TARSKI:def 2;
then - K = {[{},{}]} by Th13;
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