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 A1, NECKLA_2:def 2;
per cases ( [x,y] in the InternalRel of H1 or [x,y] in the InternalRel of H2 ) by A3, XBOOLE_0:def 3;
suppose [x,y] in the InternalRel of H1 ; :: thesis: contradiction
then y in the carrier of H1 by ZFMISC_1:87;
then y in the carrier of H1 /\ the carrier of H2 by XBOOLE_0:def 4;
hence contradiction by A2; :: thesis: verum
end;
suppose [x,y] in the InternalRel of H2 ; :: thesis: contradiction
then x in the carrier of H2 by ZFMISC_1:87;
then x in the carrier of H1 /\ the carrier of H2 by XBOOLE_0:def 4;
hence contradiction by A2; :: thesis: verum
end;
end;