let A be set ; :: thesis: for K being Element of Normal_forms_on A holds K ^ (- K) = {}

let K be Element of Normal_forms_on A; :: thesis: K ^ (- K) = {}

set x = the Element of K ^ (- K);

assume A1: K ^ (- K) <> {} ; :: thesis: contradiction

then reconsider a = the Element of K ^ (- K) as Element of DISJOINT_PAIRS A by SETWISEO:9;

consider b, c being Element of DISJOINT_PAIRS A such that

A2: b in K and

A3: c in - K and

A4: a = b \/ c by A1, NORMFORM:34;

A5: a `1 = (b `1) \/ (c `1) by A4;

A6: a `2 = (b `2) \/ (c `2) by A4;

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

g . s in (s `1) \/ (s `2) and

A8: 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 ) } ] by A3, Th11;

A9: g . b in (b `1) \/ (b `2) by A2, A7;

then a `1 meets a `2 ;

hence contradiction by NORMFORM:25; :: thesis: verum

let K be Element of Normal_forms_on A; :: thesis: K ^ (- K) = {}

set x = the Element of K ^ (- K);

assume A1: K ^ (- K) <> {} ; :: thesis: contradiction

then reconsider a = the Element of K ^ (- K) as Element of DISJOINT_PAIRS A by SETWISEO:9;

consider b, c being Element of DISJOINT_PAIRS A such that

A2: b in K and

A3: c in - K and

A4: a = b \/ c by A1, NORMFORM:34;

A5: a `1 = (b `1) \/ (c `1) by A4;

A6: a `2 = (b `2) \/ (c `2) by A4;

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

g . s in (s `1) \/ (s `2) and

A8: 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 ) } ] by A3, Th11;

A9: g . b in (b `1) \/ (b `2) by A2, A7;

now :: thesis: ( ( g . b in b `1 & g . b in a `1 & g . b in a `2 ) or ( g . b in b `2 & g . b in a `2 & g . b in a `1 ) )end;

then
(a `1) /\ (a `2) <> {}
by XBOOLE_0:def 4;per cases
( g . b in b `1 or g . b in b `2 )
by A9, XBOOLE_0:def 3;

end;

case A10:
g . b in b `1
; :: thesis: ( g . b in a `1 & g . b in a `2 )

hence
g . b in a `1
by A5, XBOOLE_0:def 3; :: thesis: g . b in a `2

g . b in { (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in K ) } by A2, A10;

then g . b in c `2 by A8;

hence g . b in a `2 by A6, XBOOLE_0:def 3; :: thesis: verum

end;g . b in { (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in K ) } by A2, A10;

then g . b in c `2 by A8;

hence g . b in a `2 by A6, XBOOLE_0:def 3; :: thesis: verum

case A11:
g . b in b `2
; :: thesis: ( g . b in a `2 & g . b in a `1 )

hence
g . b in a `2
by A6, XBOOLE_0:def 3; :: thesis: g . b in a `1

g . b in { (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in K ) } by A2, A11;

then g . b in c `1 by A8;

hence g . b in a `1 by A5, XBOOLE_0:def 3; :: thesis: verum

end;g . b in { (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in K ) } by A2, A11;

then g . b in c `1 by A8;

hence g . b in a `1 by A5, XBOOLE_0:def 3; :: thesis: verum

then a `1 meets a `2 ;

hence contradiction by NORMFORM:25; :: thesis: verum