let G be non empty RelStr ; :: thesis: for H1, H2 being RelStr st the carrier of H1 misses the carrier of H2 & ( 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) ) holds

( H1 is full SubRelStr of G & H2 is full SubRelStr of G )

let H1, H2 be RelStr ; :: thesis: ( the carrier of H1 misses the carrier of H2 & ( 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) ) implies ( H1 is full SubRelStr of G & H2 is full SubRelStr of G ) )

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: ( H1 is full SubRelStr of G & H2 is full SubRelStr of 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;

set H1H2 = [: the carrier of H1, the carrier of H2:];

set H2H1 = [: the carrier of H2, the carrier of H1:];

( H1 is full SubRelStr of G & H2 is full SubRelStr of G )

let H1, H2 be RelStr ; :: thesis: ( the carrier of H1 misses the carrier of H2 & ( 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) ) implies ( H1 is full SubRelStr of G & H2 is full SubRelStr of G ) )

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: ( H1 is full SubRelStr of G & H2 is full SubRelStr of 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;

set H1H2 = [: the carrier of H1, the carrier of H2:];

set H2H1 = [: the carrier of H2, the carrier of H1:];

per cases
( 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) )
by A2;

end;

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

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

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: verum

end;proof

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

assume A6: a in the InternalRel of G |_2 the carrier of H2 ; :: thesis: a in the InternalRel of H2

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;

end;proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in the InternalRel of G |_2 the carrier of H2 or a in the InternalRel of H2 )
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in the InternalRel of H2 or a in the InternalRel of G |_2 the carrier of H2 )

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: a in the InternalRel of G |_2 the carrier of H2

hence a in the InternalRel of G |_2 the carrier of H2 by A5, XBOOLE_0:def 4; :: thesis: verum

end;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: a in the InternalRel of G |_2 the carrier of H2

hence a in the InternalRel of G |_2 the carrier of H2 by A5, XBOOLE_0:def 4; :: thesis: verum

assume A6: a in the InternalRel of G |_2 the carrier of H2 ; :: thesis: a in the InternalRel of H2

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
( a in the InternalRel of H1 or a in the InternalRel of H2 )
by A8, XBOOLE_0:def 3;

end;

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

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: verum

end;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: verum

proof

the carrier of G = the carrier of H1 \/ the carrier of H2
by A3, NECKLA_2:def 2;
thus
the InternalRel of H1 c= the InternalRel of G |_2 the carrier of H1
:: according to XBOOLE_0:def 10 :: thesis: the InternalRel of G |_2 the carrier of H1 c= the InternalRel of H1

assume A15: a in the InternalRel of G |_2 the carrier of H1 ; :: thesis: a in the InternalRel of H1

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;

end;proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in the InternalRel of G |_2 the carrier of H1 or a in the InternalRel of H1 )
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in the InternalRel of H1 or a in the InternalRel of G |_2 the carrier of H1 )

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: a in the InternalRel of G |_2 the carrier of H1

hence a in the InternalRel of G |_2 the carrier of H1 by A14, XBOOLE_0:def 4; :: thesis: verum

end;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: a in the InternalRel of G |_2 the carrier of H1

hence a in the InternalRel of G |_2 the carrier of H1 by A14, XBOOLE_0:def 4; :: thesis: verum

assume A15: a in the InternalRel of G |_2 the carrier of H1 ; :: thesis: a in the InternalRel of H1

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
( a in the InternalRel of H1 or a in the InternalRel of H2 )
by A17, XBOOLE_0:def 3;

end;

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

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: verum

end;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: verum

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: verum

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

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

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

then A57: the InternalRel of H1 c= ( the InternalRel of H1 \/ the InternalRel of H2) \/ [: the carrier of H1, the carrier of H2:] by XBOOLE_1:4;

the carrier of G = the carrier of H1 \/ the carrier of H2 by A21, NECKLA_2:def 3;

then A58: ( the carrier of H1 c= the carrier of G & the carrier of H2 c= the carrier of G ) by XBOOLE_1:7;

A59: 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 H1 \/ the InternalRel of H2) \/ [: the carrier of H1, the carrier of H2:] c= the InternalRel of G by XBOOLE_1:7;

then the InternalRel of H1 c= the InternalRel of G by A57;

hence ( H1 is full SubRelStr of G & H2 is full SubRelStr of G ) by A59, A58, A39, A40, A22, YELLOW_0:def 13, YELLOW_0:def 14; :: thesis: verum

end;proof

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;
thus
the InternalRel of H2 c= the InternalRel of G |_2 the carrier of H2
:: according to XBOOLE_0:def 10 :: thesis: the InternalRel of G |_2 the carrier of H2 c= the InternalRel of H2

assume A24: a in the InternalRel of G |_2 the carrier of H2 ; :: thesis: a in the InternalRel of H2

then A25: a in [: the carrier of H2, the carrier of H2:] by XBOOLE_0:def 4;

a in the InternalRel of G by A24, XBOOLE_0:def 4;

then a 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 A21, NECKLA_2:def 3;

then a 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;

then ( a in the InternalRel of H1 or a 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 ( a in the InternalRel of H1 or a in 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 A26: ( a in the InternalRel of H1 or a in the InternalRel of H2 or a in [: the carrier of H1, the carrier of H2:] \/ [: the carrier of H2, the carrier of H1:] ) by XBOOLE_0:def 3;

end;proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in the InternalRel of G |_2 the carrier of H2 or a in the InternalRel of H2 )
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in the InternalRel of H2 or a in the InternalRel of G |_2 the carrier of H2 )

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: a in the InternalRel of G |_2 the carrier of H2

hence a in the InternalRel of G |_2 the carrier of H2 by A23, XBOOLE_0:def 4; :: thesis: verum

end;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: a in the InternalRel of G |_2 the carrier of H2

hence a in the InternalRel of G |_2 the carrier of H2 by A23, XBOOLE_0:def 4; :: thesis: verum

assume A24: a in the InternalRel of G |_2 the carrier of H2 ; :: thesis: a in the InternalRel of H2

then A25: a in [: the carrier of H2, the carrier of H2:] by XBOOLE_0:def 4;

a in the InternalRel of G by A24, XBOOLE_0:def 4;

then a 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 A21, NECKLA_2:def 3;

then a 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;

then ( a in the InternalRel of H1 or a 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 ( a in the InternalRel of H1 or a in 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 A26: ( a in the InternalRel of H1 or a in the InternalRel of H2 or a in [: the carrier of H1, the carrier of H2:] \/ [: the carrier of H2, the carrier of H1:] ) by XBOOLE_0:def 3;

per cases
( a in the InternalRel of H1 or a in the InternalRel of H2 or a in [: the carrier of H1, the carrier of H2:] or a in [: the carrier of H2, the carrier of H1:] )
by A26, XBOOLE_0:def 3;

end;

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

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: verum

end;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: verum

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

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: verum

end;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: verum

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

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: verum

end;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: verum

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

the InternalRel of H1 c= the InternalRel of H1 \/ ( the InternalRel of H2 \/ [: the carrier of H1, the carrier of H2:])
by XBOOLE_1:7;
thus
the InternalRel of H1 c= the InternalRel of G |_2 the carrier of H1
:: according to XBOOLE_0:def 10 :: thesis: the InternalRel of G |_2 the carrier of H1 c= the InternalRel of H1

assume A42: a in the InternalRel of G |_2 the carrier of H1 ; :: thesis: a in the InternalRel of H1

then A43: a in [: the carrier of H1, the carrier of H1:] by XBOOLE_0:def 4;

a in the InternalRel of G by A42, XBOOLE_0:def 4;

then a 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 A21, NECKLA_2:def 3;

then a 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;

then ( a in the InternalRel of H1 or a 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 ( a in the InternalRel of H1 or a in 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 A44: ( a in the InternalRel of H1 or a in the InternalRel of H2 or a in [: the carrier of H1, the carrier of H2:] \/ [: the carrier of H2, the carrier of H1:] ) by XBOOLE_0:def 3;

end;proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in the InternalRel of G |_2 the carrier of H1 or a in the InternalRel of H1 )
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in the InternalRel of H1 or a in the InternalRel of G |_2 the carrier of H1 )

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: a in the InternalRel of G |_2 the carrier of H1

hence a in the InternalRel of G |_2 the carrier of H1 by A41, XBOOLE_0:def 4; :: thesis: verum

end;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: a in the InternalRel of G |_2 the carrier of H1

hence a in the InternalRel of G |_2 the carrier of H1 by A41, XBOOLE_0:def 4; :: thesis: verum

assume A42: a in the InternalRel of G |_2 the carrier of H1 ; :: thesis: a in the InternalRel of H1

then A43: a in [: the carrier of H1, the carrier of H1:] by XBOOLE_0:def 4;

a in the InternalRel of G by A42, XBOOLE_0:def 4;

then a 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 A21, NECKLA_2:def 3;

then a 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;

then ( a in the InternalRel of H1 or a 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 ( a in the InternalRel of H1 or a in 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 A44: ( a in the InternalRel of H1 or a in the InternalRel of H2 or a in [: the carrier of H1, the carrier of H2:] \/ [: the carrier of H2, the carrier of H1:] ) by XBOOLE_0:def 3;

per cases
( a in the InternalRel of H1 or a in the InternalRel of H2 or a in [: the carrier of H1, the carrier of H2:] or a in [: the carrier of H2, the carrier of H1:] )
by A44, XBOOLE_0:def 3;

end;

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

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: verum

end;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: verum

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

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: verum

end;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: verum

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

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: verum

end;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: verum

then A57: the InternalRel of H1 c= ( the InternalRel of H1 \/ the InternalRel of H2) \/ [: the carrier of H1, the carrier of H2:] by XBOOLE_1:4;

the carrier of G = the carrier of H1 \/ the carrier of H2 by A21, NECKLA_2:def 3;

then A58: ( the carrier of H1 c= the carrier of G & the carrier of H2 c= the carrier of G ) by XBOOLE_1:7;

A59: 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 H1 \/ the InternalRel of H2) \/ [: the carrier of H1, the carrier of H2:] c= the InternalRel of G by XBOOLE_1:7;

then the InternalRel of H1 c= the InternalRel of G by A57;

hence ( H1 is full SubRelStr of G & H2 is full SubRelStr of G ) by A59, A58, A39, A40, A22, YELLOW_0:def 13, YELLOW_0:def 14; :: thesis: verum