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;

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;

end;

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;then y in the carrier of H1 /\ the carrier of H2 by XBOOLE_0:def 4;

hence contradiction by A2; :: thesis: verum

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;then x in the carrier of H1 /\ the carrier of H2 by XBOOLE_0:def 4;

hence contradiction by A2; :: thesis: verum