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 that
A1: G = union_of (H1,H2) and
A2: 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 A3: [x,y] in the InternalRel of H1 \/ the InternalRel of H2 by ;
per cases ( [x,y] in the InternalRel of H1 or [x,y] in the InternalRel of H2 ) by ;
suppose [x,y] in the InternalRel of H1 ; :: thesis: contradiction
end;
suppose [x,y] in the InternalRel of H2 ; :: thesis: contradiction
end;
end;