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 = sum_of (H1,H2) holds

not [x,y] in the InternalRel of (ComplRelStr G)

let H1, H2 be non empty RelStr ; :: thesis: for x being Element of H1

for y being Element of H2 st G = sum_of (H1,H2) holds

not [x,y] in the InternalRel of (ComplRelStr G)

let x be Element of H1; :: thesis: for y being Element of H2 st G = sum_of (H1,H2) holds

not [x,y] in the InternalRel of (ComplRelStr G)

let y be Element of H2; :: thesis: ( G = sum_of (H1,H2) implies not [x,y] in the InternalRel of (ComplRelStr G) )

set cH1 = the carrier of H1;

set cH2 = the carrier of H2;

set IH1 = the InternalRel of H1;

set IH2 = the InternalRel of H2;

[x,y] in [: the carrier of H1, the carrier of H2:] \/ [: the carrier of H2, the carrier of H1:] by XBOOLE_0:def 3;

then [x,y] in the InternalRel of H2 \/ ([: the carrier of H1, the carrier of H2:] \/ [: the carrier of H2, the carrier of H1:]) by XBOOLE_0:def 3;

then [x,y] in the InternalRel of H1 \/ ( the InternalRel of H2 \/ ([: the carrier of H1, the carrier of H2:] \/ [: the carrier of H2, the carrier of H1:])) by XBOOLE_0:def 3;

then [x,y] in the InternalRel of H1 \/ (( the InternalRel of H2 \/ [: the carrier of H1, the carrier of H2:]) \/ [: the carrier of H2, the carrier of H1:]) by XBOOLE_1:4;

then A1: [x,y] in (( the InternalRel of H1 \/ the InternalRel of H2) \/ [: the carrier of H1, the carrier of H2:]) \/ [: the carrier of H2, the carrier of H1:] by XBOOLE_1:113;

assume G = sum_of (H1,H2) ; :: thesis: not [x,y] in the InternalRel of (ComplRelStr G)

then A2: [x,y] in the InternalRel of G by A1, NECKLA_2:def 3;

not [x,y] in the InternalRel of (ComplRelStr G)

for x being Element of H1

for y being Element of H2 st G = sum_of (H1,H2) holds

not [x,y] in the InternalRel of (ComplRelStr G)

let H1, H2 be non empty RelStr ; :: thesis: for x being Element of H1

for y being Element of H2 st G = sum_of (H1,H2) holds

not [x,y] in the InternalRel of (ComplRelStr G)

let x be Element of H1; :: thesis: for y being Element of H2 st G = sum_of (H1,H2) holds

not [x,y] in the InternalRel of (ComplRelStr G)

let y be Element of H2; :: thesis: ( G = sum_of (H1,H2) implies not [x,y] in the InternalRel of (ComplRelStr G) )

set cH1 = the carrier of H1;

set cH2 = the carrier of H2;

set IH1 = the InternalRel of H1;

set IH2 = the InternalRel of H2;

[x,y] in [: the carrier of H1, the carrier of H2:] \/ [: the carrier of H2, the carrier of H1:] by XBOOLE_0:def 3;

then [x,y] in the InternalRel of H2 \/ ([: the carrier of H1, the carrier of H2:] \/ [: the carrier of H2, the carrier of H1:]) by XBOOLE_0:def 3;

then [x,y] in the InternalRel of H1 \/ ( the InternalRel of H2 \/ ([: the carrier of H1, the carrier of H2:] \/ [: the carrier of H2, the carrier of H1:])) by XBOOLE_0:def 3;

then [x,y] in the InternalRel of H1 \/ (( the InternalRel of H2 \/ [: the carrier of H1, the carrier of H2:]) \/ [: the carrier of H2, the carrier of H1:]) by XBOOLE_1:4;

then A1: [x,y] in (( the InternalRel of H1 \/ the InternalRel of H2) \/ [: the carrier of H1, the carrier of H2:]) \/ [: the carrier of H2, the carrier of H1:] by XBOOLE_1:113;

assume G = sum_of (H1,H2) ; :: thesis: not [x,y] in the InternalRel of (ComplRelStr G)

then A2: [x,y] in the InternalRel of G by A1, NECKLA_2:def 3;

not [x,y] in the InternalRel of (ComplRelStr G)

proof

hence
not [x,y] in the InternalRel of (ComplRelStr G)
; :: thesis: verum
assume
[x,y] in the InternalRel of (ComplRelStr G)
; :: thesis: contradiction

then [x,y] in the InternalRel of G /\ the InternalRel of (ComplRelStr G) by A2, XBOOLE_0:def 4;

then the InternalRel of G meets the InternalRel of (ComplRelStr G) ;

hence contradiction by Th12; :: thesis: verum

end;then [x,y] in the InternalRel of G /\ the InternalRel of (ComplRelStr G) by A2, XBOOLE_0:def 4;

then the InternalRel of G meets the InternalRel of (ComplRelStr G) ;

hence contradiction by Th12; :: thesis: verum