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) )
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 A1: [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;
assume G = sum_of (H1,H2) ; :: thesis: not [x,y] in the InternalRel of (ComplRelStr G)
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) ;
hence contradiction by Th12; :: thesis: verum
end;
hence not [x,y] in the InternalRel of (ComplRelStr G) ; :: thesis: verum