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 A3:
RelStr(# the
carrier of
G, the
InternalRel of
G #)
= union_of (
H1,
H2)
;
( 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
XBOOLE_0:def 10 the InternalRel of G |_2 the carrier of H2 c= the InternalRel of H2
let a be
set ;
TARSKI:def 3 ( 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
;
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;
suppose
a in the
InternalRel of
H1
;
a in the InternalRel of H2then consider x,
y being
set 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
set 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, ZFMISC_1:27;
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, XBOOLE_0:def 7;
verum end;
end; A13:
the
InternalRel of
H1 = the
InternalRel of
G |_2 the
carrier of
H1
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;
verum end; 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
set ;
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;
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;
suppose
a in the
InternalRel of
H1
;
a in the InternalRel of H2then consider x,
y being
set 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
set 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, ZFMISC_1:27;
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, XBOOLE_0:def 7;
verum end; suppose
a in [: the carrier of H1, the carrier of H2:]
;
a in the InternalRel of H2then consider x,
y being
set 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
set 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, ZFMISC_1:27;
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, XBOOLE_0:def 7;
verum end; suppose
a in [: the carrier of H2, the carrier of H1:]
;
a in the InternalRel of H2then consider x,
y being
set 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
set 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, ZFMISC_1:27;
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, XBOOLE_0:def 7;
verum end;
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
set ;
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;
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;
suppose
a in the
InternalRel of
H2
;
a in the InternalRel of H1then consider x,
y being
set 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
set 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, ZFMISC_1:27;
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, XBOOLE_0:def 7;
verum end; suppose
a in [: the carrier of H1, the carrier of H2:]
;
a in the InternalRel of H1then consider x,
y being
set 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
set 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, ZFMISC_1:27;
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, XBOOLE_0:def 7;
verum end; suppose
a in [: the carrier of H2, the carrier of H1:]
;
a in the InternalRel of H1then consider x,
y being
set 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
set 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, ZFMISC_1:27;
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, XBOOLE_0:def 7;
verum 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 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, XBOOLE_1:1;
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;