let G be non empty RelStr ; :: thesis:
let H1, H2 be RelStr ; :: thesis:
assume that
A1: the carrier of H1 misses the carrier of H2 and
A2: ( RelStr(# the carrier of G, the InternalRel of G #) = union_of (H1,H2) or RelStr(# the carrier of G, the InternalRel of G #) = sum_of (H1,H2) ) ; :: thesis:
set cH1 = the carrier of H1;
set cH2 = the carrier of H2;
set IH1 = the InternalRel of H1;
set IH2 = the InternalRel of H2;
set H1H2 = [: the carrier of H1, the carrier of H2:];
set H2H1 = [: the carrier of H2, the carrier of H1:];

per cases by A2;

suppose A3: RelStr(# the carrier of G, the InternalRel of G #) = union_of (H1,H2) ; :: thesis:

A4: the InternalRel of H2 = the InternalRel of G |_2 the carrier of H2

proof

thus the InternalRel of H2 c= the InternalRel of G |_2 the carrier of H2 :: according to XBOOLE_0:def 10 :: thesis:

proof

let a be object ; :: according to TARSKI:def 3 :: thesis:
the InternalRel of G = the InternalRel of H1 \/ the InternalRel of H2 by A3, NECKLA_2:def 2;
then A5: the InternalRel of H2 c= the InternalRel of G by XBOOLE_1:7;
assume a in the InternalRel of H2 ; :: thesis:
hence a in the InternalRel of G |_2 the carrier of H2 by A5, XBOOLE_0:def 4; :: thesis:

end;

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume A6: a in the InternalRel of G |_2 the carrier of H2 ; :: thesis:
then A7: a in [: the carrier of H2, the carrier of H2:] by XBOOLE_0:def 4;
a in the InternalRel of G by A6, XBOOLE_0:def 4;
then A8: a in the InternalRel of H1 \/ the InternalRel of H2 by A3, NECKLA_2:def 2;

per cases by A8, XBOOLE_0:def 3;

suppose a in the InternalRel of H1 ; :: thesis:

then consider x, y being object such that
A9: a = [x,y] and
A10: x in the carrier of H1 and
y in the carrier of H1 by RELSET_1:2;
consider x1, y1 being object such that
A11: x1 in the carrier of H2 and
y1 in the carrier of H2 and
A12: a = [x1,y1] by A7, ZFMISC_1:def 2;
x = x1 by A9, A12, XTUPLE_0:1;
then the carrier of H1 /\ the carrier of H2 <> {} by A10, A11, XBOOLE_0:def 4;
hence a in the InternalRel of H2 by A1; :: thesis:

end;

suppose a in the InternalRel of H2 ; :: thesis:

hence a in the InternalRel of H2 ; :: thesis:

end;

A13: the InternalRel of H1 = the InternalRel of G |_2 the carrier of H1

proof

thus the InternalRel of H1 c= the InternalRel of G |_2 the carrier of H1 :: according to XBOOLE_0:def 10 :: thesis:

proof

let a be object ; :: according to TARSKI:def 3 :: thesis:
the InternalRel of G = the InternalRel of H1 \/ the InternalRel of H2 by A3, NECKLA_2:def 2;
then A14: the InternalRel of H1 c= the InternalRel of G by XBOOLE_1:7;
assume a in the InternalRel of H1 ; :: thesis:
hence a in the InternalRel of G |_2 the carrier of H1 by A14, XBOOLE_0:def 4; :: thesis:

end;

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume A15: a in the InternalRel of G |_2 the carrier of H1 ; :: thesis:
then A16: a in [: the carrier of H1, the carrier of H1:] by XBOOLE_0:def 4;
a in the InternalRel of G by A15, XBOOLE_0:def 4;
then A17: a in the InternalRel of H1 \/ the InternalRel of H2 by A3, NECKLA_2:def 2;

per cases by A17, XBOOLE_0:def 3;

suppose a in the InternalRel of H1 ; :: thesis:

hence a in the InternalRel of H1 ; :: thesis:

end;

suppose a in the InternalRel of H2 ; :: thesis:

then consider x, y being object such that
A18: a = [x,y] and
A19: x in the carrier of H2 and
y in the carrier of H2 by RELSET_1:2;
ex x1, y1 being object st
( x1 in the carrier of H1 & y1 in the carrier of H1 & a = [x1,y1] ) by A16, ZFMISC_1:def 2;
then x in the carrier of H1 by A18, XTUPLE_0:1;
hence a in the InternalRel of H1 by A1, A19, XBOOLE_0:3; :: thesis:

end;

the carrier of G = the carrier of H1 \/ the carrier of H2 by A3, NECKLA_2:def 2;
then A20: ( the carrier of H1 c= the carrier of G & the carrier of H2 c= the carrier of G ) by XBOOLE_1:7;
the InternalRel of G = the InternalRel of H1 \/ the InternalRel of H2 by A3, NECKLA_2:def 2;
then ( the InternalRel of H1 c= the InternalRel of G & the InternalRel of H2 c= the InternalRel of G ) by XBOOLE_1:7;
hence ( H1 is full SubRelStr of G & H2 is full SubRelStr of G ) by A20, A13, A4, YELLOW_0:def 13, YELLOW_0:def 14; :: thesis:

end;

suppose A21: RelStr(# the carrier of G, the InternalRel of G #) = sum_of (H1,H2) ; :: thesis:

A22: the InternalRel of H2 = the InternalRel of G |_2 the carrier of H2

proof

thus the InternalRel of H2 c= the InternalRel of G |_2 the carrier of H2 :: according to XBOOLE_0:def 10 :: thesis:

proof

let a be object ; :: according to TARSKI:def 3 :: thesis:
the InternalRel of G = (( 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 A21, NECKLA_2:def 3;
then the InternalRel of G = the InternalRel of H2 \/ (( the InternalRel of H1 \/ [: the carrier of H1, the carrier of H2:]) \/ [: the carrier of H2, the carrier of H1:]) by XBOOLE_1:113;
then A23: the InternalRel of H2 c= the InternalRel of G by XBOOLE_1:7;
assume a in the InternalRel of H2 ; :: thesis:
hence a in the InternalRel of G |_2 the carrier of H2 by A23, XBOOLE_0:def 4; :: thesis:

end;

per cases by A26, XBOOLE_0:def 3;

suppose a in the InternalRel of H1 ; :: thesis:

then consider x, y being object such that
A27: a = [x,y] and
A28: x in the carrier of H1 and
y in the carrier of H1 by RELSET_1:2;
consider x1, y1 being object such that
A29: x1 in the carrier of H2 and
y1 in the carrier of H2 and
A30: a = [x1,y1] by A25, ZFMISC_1:def 2;
x = x1 by A27, A30, XTUPLE_0:1;
then the carrier of H1 /\ the carrier of H2 <> {} by A28, A29, XBOOLE_0:def 4;
hence a in the InternalRel of H2 by A1; :: thesis:

end;

suppose a in the InternalRel of H2 ; :: thesis:

hence a in the InternalRel of H2 ; :: thesis:

end;

suppose a in [: the carrier of H1, the carrier of H2:] ; :: thesis:

then consider x, y being object such that
A31: x in the carrier of H1 and
y in the carrier of H2 and
A32: a = [x,y] by ZFMISC_1:def 2;
consider x1, y1 being object such that
A33: x1 in the carrier of H2 and
y1 in the carrier of H2 and
A34: a = [x1,y1] by A25, ZFMISC_1:def 2;
x = x1 by A32, A34, XTUPLE_0:1;
then the carrier of H1 /\ the carrier of H2 <> {} by A31, A33, XBOOLE_0:def 4;
hence a in the InternalRel of H2 by A1; :: thesis:

end;

suppose a in [: the carrier of H2, the carrier of H1:] ; :: thesis:

then consider x, y being object such that
x in the carrier of H2 and
A35: y in the carrier of H1 and
A36: a = [x,y] by ZFMISC_1:def 2;
consider x1, y1 being object such that
x1 in the carrier of H2 and
A37: y1 in the carrier of H2 and
A38: a = [x1,y1] by A25, ZFMISC_1:def 2;
y = y1 by A36, A38, XTUPLE_0:1;
then the carrier of H1 /\ the carrier of H2 <> {} by A35, A37, XBOOLE_0:def 4;
hence a in the InternalRel of H2 by A1; :: thesis:

end;

the InternalRel of H2 c= ( the InternalRel of H1 \/ the InternalRel of H2) \/ [: the carrier of H1, the carrier of H2:] by XBOOLE_1:7, XBOOLE_1:10;
then A39: the InternalRel of H2 c= (( 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:10;
A40: the InternalRel of H1 = the InternalRel of G |_2 the carrier of H1

proof

thus the InternalRel of H1 c= the InternalRel of G |_2 the carrier of H1 :: according to XBOOLE_0:def 10 :: thesis:

proof

let a be object ; :: according to TARSKI:def 3 :: thesis:
the InternalRel of G = (( 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 A21, NECKLA_2:def 3
.= 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 ;
then A41: the InternalRel of H1 c= the InternalRel of G by XBOOLE_1:7;
assume a in the InternalRel of H1 ; :: thesis:
hence a in the InternalRel of G |_2 the carrier of H1 by A41, XBOOLE_0:def 4; :: thesis:

end;

per cases by A44, XBOOLE_0:def 3;

suppose a in the InternalRel of H1 ; :: thesis:

hence a in the InternalRel of H1 ; :: thesis:

end;

suppose a in the InternalRel of H2 ; :: thesis:

then consider x, y being object such that
A45: a = [x,y] and
A46: x in the carrier of H2 and
y in the carrier of H2 by RELSET_1:2;
consider x1, y1 being object such that
A47: x1 in the carrier of H1 and
y1 in the carrier of H1 and
A48: a = [x1,y1] by A43, ZFMISC_1:def 2;
x = x1 by A45, A48, XTUPLE_0:1;
then the carrier of H1 /\ the carrier of H2 <> {} by A46, A47, XBOOLE_0:def 4;
hence a in the InternalRel of H1 by A1; :: thesis:

end;

suppose a in [: the carrier of H1, the carrier of H2:] ; :: thesis:

then consider x, y being object such that
x in the carrier of H1 and
A49: y in the carrier of H2 and
A50: a = [x,y] by ZFMISC_1:def 2;
consider x1, y1 being object such that
x1 in the carrier of H1 and
A51: y1 in the carrier of H1 and
A52: a = [x1,y1] by A43, ZFMISC_1:def 2;
y = y1 by A50, A52, XTUPLE_0:1;
then the carrier of H1 /\ the carrier of H2 <> {} by A49, A51, XBOOLE_0:def 4;
hence a in the InternalRel of H1 by A1; :: thesis:

end;

suppose a in [: the carrier of H2, the carrier of H1:] ; :: thesis:

then consider x, y being object such that
A53: x in the carrier of H2 and
y in the carrier of H1 and
A54: a = [x,y] by ZFMISC_1:def 2;
consider x1, y1 being object such that
A55: x1 in the carrier of H1 and
y1 in the carrier of H1 and
A56: a = [x1,y1] by A43, ZFMISC_1:def 2;
x = x1 by A54, A56, XTUPLE_0:1;
then the carrier of H1 /\ the carrier of H2 <> {} by A53, A55, XBOOLE_0:def 4;
hence a in the InternalRel of H1 by A1; :: thesis:

end;

end;