let G be RelStr ; 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 ; 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; 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; ( 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
; not [x,y] in the InternalRel of G
assume
[x,y] in the InternalRel of G
; contradiction
then A3:
[x,y] in the InternalRel of H1 \/ the InternalRel of H2
by A1, NECKLA_2:def 2;