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 ()

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 ()

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 ()

let y be Element of H2; :: thesis: ( G = sum_of (H1,H2) implies not [x,y] in the InternalRel of () )
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 ()
then A2: [x,y] in the InternalRel of G by ;
not [x,y] in the InternalRel of ()
proof
assume [x,y] in the InternalRel of () ; :: thesis: contradiction
then [x,y] in the InternalRel of G /\ the InternalRel of () by ;
then the InternalRel of G meets the InternalRel of () ;
hence contradiction by Th12; :: thesis: verum
end;
hence not [x,y] in the InternalRel of () ; :: thesis: verum