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) = {}
consider x being Element of K ^ (- K);
assume A1: K ^ (- K) <> {} ; :: thesis: contradiction
then reconsider a = x as Element of DISJOINT_PAIRS A by SETWISEO:14;
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:55;
A5: a `1 = (b `1 ) \/ (c `1 ) by A4, MCART_1:7;
A6: a `2 = (b `2 ) \/ (c `2 ) by A4, MCART_1:7;
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, Th16;
A9: g . b in (b `1 ) \/ (b `2 ) by A2, A7;

now

per cases ( g . b in b `1 or g . b in b `2 ) by A9, XBOOLE_0:def 3;

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, MCART_1:7;
hence g . b in a `2 by A6, XBOOLE_0:def 3; :: thesis: verum

end;

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, MCART_1:7;
hence g . b in a `1 by A5, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

then (a `1 ) /\ (a `2 ) <> {} by XBOOLE_0:def 4;
then a `1 meets a `2 by XBOOLE_0:def 7;
hence contradiction by NORMFORM:44; :: thesis: verum