let A be set ; :: thesis: for K being Element of Normal_forms_on A st K = {} holds
- K = {[{},{}]}
let K be Element of Normal_forms_on A; :: thesis: ( K = {} implies - K = {[{},{}]} )
assume A1: K = {} ; :: thesis: - K = {[{},{}]}
A2: { [ { (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 ) } ] where g 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) } = {[{},{}]}

proof

thus { [ { (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 ) } ] where g 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) } c= {[{},{}]} :: according to XBOOLE_0:def 10 :: thesis: {[{},{}]} 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 ) } ] where g 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) }

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 ) } , { (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in K ) } ] where g 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) } or x in {[{},{}]} )
assume x in { [ { (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 ) } ] where g 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) } ; :: thesis: x in {[{},{}]}
then consider g being Element of Funcs ((DISJOINT_PAIRS A),[A]) such that
A3: x = [ { (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 ) } ] and
for s being Element of DISJOINT_PAIRS A st s in K holds
g . s in (s `1) \/ (s `2) ;
A4: x `2 = { (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in K ) } by A3, MCART_1:7;

A5: now

consider y being Element of x `2 ;
assume x `2 <> {} ; :: thesis: contradiction
then y in x `2 ;
then ex t1 being Element of DISJOINT_PAIRS A st
( y = g . t1 & g . t1 in t1 `1 & t1 in K ) by A4;
hence contradiction by A1; :: thesis: verum

end;

A6: x `1 = { (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in K ) } by A3, MCART_1:7;

now

consider y being Element of x `1 ;
assume x `1 <> {} ; :: thesis: contradiction
then y in x `1 ;
then ex t1 being Element of DISJOINT_PAIRS A st
( y = g . t1 & g . t1 in t1 `2 & t1 in K ) by A6;
hence contradiction by A1; :: thesis: verum

end;

then x = [{},{}] by A3, A5, MCART_1:8;
hence x in {[{},{}]} by TARSKI:def 1; :: thesis: verum

end;

thus {[{},{}]} 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 ) } ] where g 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) } :: thesis: verum

proof

consider g being Element of Funcs ((DISJOINT_PAIRS A),[A]);
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {[{},{}]} or x in { [ { (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 ) } ] where g 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) } )
assume x in {[{},{}]} ; :: thesis: x in { [ { (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 ) } ] where g 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) }
then A7: x = [{},{}] by TARSKI:def 1;

A8: now

consider y being Element of { (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in K ) } ;
assume { (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in K ) } <> {} ; :: thesis: contradiction
then y in { (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in K ) } ;
then ex t1 being Element of DISJOINT_PAIRS A st
( y = g . t1 & g . t1 in t1 `2 & t1 in K ) ;
hence contradiction by A1; :: thesis: verum

end;

A9: now

consider y being Element of { (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in K ) } ;
assume { (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in K ) } <> {} ; :: thesis: contradiction
then y in { (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in K ) } ;
then ex t1 being Element of DISJOINT_PAIRS A st
( y = g . t1 & g . t1 in t1 `1 & t1 in K ) ;
hence contradiction by A1; :: thesis: verum

end;

for s being Element of DISJOINT_PAIRS A st s in K holds
g . s in (s `1) \/ (s `2) by A1;
hence x in { [ { (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 ) } ] where g 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) } by A7, A8, A9; :: thesis: verum

end;

end;

[{},{}] is Element of DISJOINT_PAIRS A by Th17;
hence - K = {[{},{}]} by A2, ZFMISC_1:52; :: thesis: verum