let G be non empty RelStr ; 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 ; ( 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) )
; ( 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 A21:
RelStr(# the
carrier of
G, the
InternalRel of
G #)
= sum_of (
H1,
H2)
;
( 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
XBOOLE_0:def 10 the InternalRel of G |_2 the carrier of H2 c= the InternalRel of H2
let a be
object ;
TARSKI:def 3 ( 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
;
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;
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
XBOOLE_0:def 10 the InternalRel of G |_2 the carrier of H1 c= the InternalRel of H1
let a be
object ;
TARSKI:def 3 ( 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
;
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;
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 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;
verum end; end;