let G be RelStr ; :: thesis: for H1, H2 being non empty RelStr
for x being Element of H1
for y being Element of H2 st G = sum_of H1,H2 holds
not [x,y] in the InternalRel of (ComplRelStr G)
let H1, H2 be non empty RelStr ; :: thesis: for x being Element of H1
for y being Element of H2 st G = sum_of H1,H2 holds
not [x,y] in the InternalRel of (ComplRelStr G)
let x be Element of H1; :: thesis: for y being Element of H2 st G = sum_of H1,H2 holds
not [x,y] in the InternalRel of (ComplRelStr G)
let y be Element of H2; :: thesis: ( G = sum_of H1,H2 implies not [x,y] in the InternalRel of (ComplRelStr G) )
assume A1: G = sum_of H1,H2 ; :: thesis: not [x,y] in the InternalRel of (ComplRelStr G)
set cH1 = the carrier of H1;
set cH2 = the carrier of H2;
set IH1 = the InternalRel of H1;
set IH2 = the InternalRel of H2;
[x,y] in [:the carrier of H1,the carrier of H2:] \/ [:the carrier of H2,the carrier of H1:] by XBOOLE_0:def 3;
then [x,y] in the InternalRel of H2 \/ ([:the carrier of H1,the carrier of H2:] \/ [:the carrier of H2,the carrier of H1:]) by XBOOLE_0:def 3;
then [x,y] in the InternalRel of H1 \/ (the InternalRel of H2 \/ ([:the carrier of H1,the carrier of H2:] \/ [:the carrier of H2,the carrier of H1:])) by XBOOLE_0:def 3;
then [x,y] in the InternalRel of H1 \/ ((the InternalRel of H2 \/ [:the carrier of H1,the carrier of H2:]) \/ [:the carrier of H2,the carrier of H1:]) by XBOOLE_1:4;
then [x,y] in ((the InternalRel of H1 \/ the InternalRel of H2) \/ [:the carrier of H1,the carrier of H2:]) \/ [:the carrier of H2,the carrier of H1:] by XBOOLE_1:113;
then A2: [x,y] in the InternalRel of G by A1, NECKLA_2:def 3;
not [x,y] in the InternalRel of (ComplRelStr G)

proof

assume [x,y] in the InternalRel of (ComplRelStr G) ; :: thesis: contradiction
then [x,y] in the InternalRel of G /\ the InternalRel of (ComplRelStr G) by A2, XBOOLE_0:def 4;
then the InternalRel of G meets the InternalRel of (ComplRelStr G) by XBOOLE_0:def 7;
hence contradiction by Th12; :: thesis: verum

end;

hence not [x,y] in the InternalRel of (ComplRelStr G) ; :: thesis: verum