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 )

( b in - K & b c= a ) ; :: thesis: verum

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 )end;

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

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

end;

suppose A2:
not A is empty
; :: thesis: ex c being Element of DISJOINT_PAIRS A st

( c in - K & c c= a )

( c in - K & c c= a )

defpred S_{1}[ set , set ] means $2 in (($1 `1) /\ (a `2)) \/ (($1 `2) /\ (a `1));

A3: A = [A] by A2, Def2;

A7: for s being Element of DISJOINT_PAIRS A st s in K holds

S_{1}[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

take c = c; :: thesis: ( c in - K & c c= a )

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;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_{1}[s,x]

consider g being Element of Funcs ((DISJOINT_PAIRS A),[A]) such that ex x being Element of [A] st S

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_{1}[s,x] )

assume s in K ; :: thesis: ex x being Element of [A] st S_{1}[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_{1}[s,x]

( x in (s `1) /\ (a `2) or x in (s `2) /\ (a `1) ) by A6, XBOOLE_0:def 4;

hence S_{1}[s,x]
by XBOOLE_0:def 3; :: thesis: verum

end;let s be Element of DISJOINT_PAIRS A; :: thesis: ( s in K implies ex x being Element of [A] st S

assume s in K ; :: thesis: ex x being Element of [A] st S

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

( x in (s `1) /\ (a `2) or x in (s `2) /\ (a `1) ) by A6, XBOOLE_0:def 4;

hence S

A7: for s being Element of DISJOINT_PAIRS A st s in K holds

S

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

A11:
{ (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in K ) } c= a `1
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;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

proof

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

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)

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

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

suppose A14:
A is empty
; :: thesis: ex b being Element of DISJOINT_PAIRS A st

( b in - K & b c= a )

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

( b in - K & b c= a ) ; :: thesis: verum