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 = union_of H1,H2 & the carrier of H1 misses the carrier of H2 holds
not [x,y] in the InternalRel of G
let H1, H2 be non empty RelStr ; :: thesis: for x being Element of H1
for y being Element of H2 st G = union_of H1,H2 & the carrier of H1 misses the carrier of H2 holds
not [x,y] in the InternalRel of G
let x be Element of H1; :: thesis: for y being Element of H2 st G = union_of H1,H2 & the carrier of H1 misses the carrier of H2 holds
not [x,y] in the InternalRel of G
let y be Element of H2; :: thesis: ( G = union_of H1,H2 & the carrier of H1 misses the carrier of H2 implies not [x,y] in the InternalRel of G )
assume A1: ( G = union_of H1,H2 & the carrier of H1 misses the carrier of H2 ) ; :: thesis: not [x,y] in the InternalRel of G
assume [x,y] in the InternalRel of G ; :: thesis: contradiction
then A2: [x,y] in the InternalRel of H1 \/ the InternalRel of H2 by A1, NECKLA_2:def 2;

per cases ( [x,y] in the InternalRel of H1 or [x,y] in the InternalRel of H2 ) by A2, XBOOLE_0:def 3;

suppose [x,y] in the InternalRel of H1 ; :: thesis: contradiction

then ( x in the carrier of H1 & y in the carrier of H1 ) by ZFMISC_1:106;
then y in the carrier of H1 /\ the carrier of H2 by XBOOLE_0:def 4;
hence contradiction by A1, XBOOLE_0:def 7; :: thesis: verum

end;

suppose [x,y] in the InternalRel of H2 ; :: thesis: contradiction

then ( x in the carrier of H2 & y in the carrier of H2 ) by ZFMISC_1:106;
then x in the carrier of H1 /\ the carrier of H2 by XBOOLE_0:def 4;
hence contradiction by A1, XBOOLE_0:def 7; :: thesis: verum

end;

end;