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:];
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;
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
proof
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
proof
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 ;
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 ; :: thesis: verum
end;
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 )
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 ;
then A8: a in the InternalRel of H1 \/ the InternalRel of H2 by ;
per cases ( a in the InternalRel of H1 or a in the InternalRel of H2 ) by ;
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 ;
x = x1 by ;
then the carrier of H1 /\ the carrier of H2 <> {} by ;
hence a in the InternalRel of H2 by A1; :: thesis: verum
end;
suppose a in the InternalRel of H2 ; :: thesis: a in the InternalRel of H2
hence a in the InternalRel of H2 ; :: thesis: verum
end;
end;
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: the InternalRel of G |_2 the carrier of H1 c= the InternalRel of H1
proof
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 ;
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 ; :: thesis: verum
end;
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 )
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 ;
then A17: a in the InternalRel of H1 \/ the InternalRel of H2 by ;
per cases ( a in the InternalRel of H1 or a in the InternalRel of H2 ) by ;
suppose a in the InternalRel of H1 ; :: thesis: a in the InternalRel of H1
hence a in the InternalRel of H1 ; :: thesis: verum
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 ;
then x in the carrier of H1 by ;
hence a in the InternalRel of H1 by ; :: thesis: verum
end;
end;
end;
the carrier of G = the carrier of H1 \/ the carrier of H2 by ;
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 ;
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 ; :: thesis: verum
end;
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
proof
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
proof
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 ;
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 ; :: thesis: verum
end;
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 )
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 ;
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 ;
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 ;
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 ;
x = x1 by ;
then the carrier of H1 /\ the carrier of H2 <> {} by ;
hence a in the InternalRel of H2 by A1; :: thesis: verum
end;
suppose a in the InternalRel of H2 ; :: thesis: a in the InternalRel of H2
hence a in the InternalRel of H2 ; :: thesis: verum
end;
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 ;
x = x1 by ;
then the carrier of H1 /\ the carrier of H2 <> {} by ;
hence a in the InternalRel of H2 by A1; :: thesis: verum
end;
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 ;
y = y1 by ;
then the carrier of H1 /\ the carrier of H2 <> {} by ;
hence a in the InternalRel of H2 by A1; :: thesis: verum
end;
end;
end;
the InternalRel of H2 c= ( the InternalRel of H1 \/ the InternalRel of H2) \/ [: the carrier of H1, the carrier of H2:] by ;
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: the InternalRel of G |_2 the carrier of H1 c= the InternalRel of H1
proof
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
.= 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 ; :: thesis: verum
end;
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 )
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 ;
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 ;
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 ;
suppose a in the InternalRel of H1 ; :: thesis: a in the InternalRel of H1
hence a in the InternalRel of H1 ; :: thesis: verum
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 ;
x = x1 by ;
then the carrier of H1 /\ the carrier of H2 <> {} by ;
hence a in the InternalRel of H1 by A1; :: thesis: verum
end;
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 ;
y = y1 by ;
then the carrier of H1 /\ the carrier of H2 <> {} by ;
hence a in the InternalRel of H1 by A1; :: thesis: verum
end;
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 ;
x = x1 by ;
then the carrier of H1 /\ the carrier of H2 <> {} by ;
hence a in the InternalRel of H1 by A1; :: thesis: verum
end;
end;
end;
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;
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 ;
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 ;
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 ; :: thesis: verum
end;
end;