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 )then A4:
the
InternalRel of
G = the
InternalRel of
H1 \/ the
InternalRel of
H2
by NECKLA_2:def 2;
then A5:
the
InternalRel of
H1 c= the
InternalRel of
G
by XBOOLE_1:7;
A6:
the
carrier of
G = the
carrier of
H1 \/ the
carrier of
H2
by A3, NECKLA_2:def 2;
then A7:
the
carrier of
H1 c= the
carrier of
G
by XBOOLE_1:7;
A8:
the
carrier of
H2 c= the
carrier of
G
by A6, XBOOLE_1:7;
A9:
the
InternalRel of
H2 c= the
InternalRel of
G
by A4, XBOOLE_1:7;
A10:
the
InternalRel of
H1 = the
InternalRel of
G |_2 the
carrier of
H1
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
let a be
set ;
:: 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
a in the
InternalRel of
G |_2 the
carrier of
H2
;
:: thesis: a in the InternalRel of H2
then A17:
(
a in the
InternalRel of
G &
a in [:the carrier of H2,the carrier of H2:] )
by XBOOLE_0:def 4;
then A18:
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 A18, XBOOLE_0:def 3;
suppose
a in the
InternalRel of
H1
;
:: thesis: a in the InternalRel of H2then consider x,
y being
set such that A19:
(
a = [x,y] &
x in the
carrier of
H1 &
y in the
carrier of
H1 )
by RELSET_1:6;
consider x1,
y1 being
set such that A20:
(
x1 in the
carrier of
H2 &
y1 in the
carrier of
H2 &
a = [x1,y1] )
by A17, ZFMISC_1:def 2;
(
x = x1 &
y = y1 )
by A19, A20, ZFMISC_1:33;
then
the
carrier of
H1 /\ the
carrier of
H2 <> {}
by A19, A20, XBOOLE_0:def 4;
hence
a in the
InternalRel of
H2
by A1, XBOOLE_0:def 7;
:: thesis: verum end;
end; hence
(
H1 is
full SubRelStr of
G &
H2 is
full SubRelStr of
G )
by A5, A7, A8, A9, A10, YELLOW_0:def 13, YELLOW_0:def 14;
:: 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 )then A22:
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 NECKLA_2:def 3;
then A23:
(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;
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
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;
then A24:
the
InternalRel of
H1 c= the
InternalRel of
G
by A23, XBOOLE_1:1;
A25:
the
carrier of
G = the
carrier of
H1 \/ the
carrier of
H2
by A21, NECKLA_2:def 3;
then A26:
the
carrier of
H1 c= the
carrier of
G
by XBOOLE_1:7;
A27:
the
carrier of
H2 c= the
carrier of
G
by A25, XBOOLE_1:7;
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
the
InternalRel of
H2 c= (the InternalRel of H1 \/ the InternalRel of H2) \/ [:the carrier of H1,the carrier of H2:]
by XBOOLE_1:4;
then A28:
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;
A29:
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
let a be
set ;
:: 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
a in the
InternalRel of
G |_2 the
carrier of
H1
;
:: thesis: a in the InternalRel of H1
then A31:
(
a in the
InternalRel of
G &
a in [:the carrier of H1,the carrier of H1:] )
by 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 A32:
(
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 A32, XBOOLE_0:def 3;
suppose
a in the
InternalRel of
H2
;
:: thesis: a in the InternalRel of H1then consider x,
y being
set such that A33:
(
a = [x,y] &
x in the
carrier of
H2 &
y in the
carrier of
H2 )
by RELSET_1:6;
consider x1,
y1 being
set such that A34:
(
x1 in the
carrier of
H1 &
y1 in the
carrier of
H1 &
a = [x1,y1] )
by A31, ZFMISC_1:def 2;
(
x = x1 &
y = y1 )
by A33, A34, ZFMISC_1:33;
then
the
carrier of
H1 /\ the
carrier of
H2 <> {}
by A33, A34, XBOOLE_0:def 4;
hence
a in the
InternalRel of
H1
by A1, XBOOLE_0:def 7;
:: thesis: verum end; suppose
a in [:the carrier of H1,the carrier of H2:]
;
:: thesis: a in the InternalRel of H1then consider x,
y being
set such that A35:
(
x in the
carrier of
H1 &
y in the
carrier of
H2 &
a = [x,y] )
by ZFMISC_1:def 2;
consider x1,
y1 being
set such that A36:
(
x1 in the
carrier of
H1 &
y1 in the
carrier of
H1 &
a = [x1,y1] )
by A31, ZFMISC_1:def 2;
(
x = x1 &
y = y1 )
by A35, A36, ZFMISC_1:33;
then
the
carrier of
H1 /\ the
carrier of
H2 <> {}
by A35, A36, XBOOLE_0:def 4;
hence
a in the
InternalRel of
H1
by A1, XBOOLE_0:def 7;
:: thesis: verum end; suppose
a in [:the carrier of H2,the carrier of H1:]
;
:: thesis: a in the InternalRel of H1then consider x,
y being
set such that A37:
(
x in the
carrier of
H2 &
y in the
carrier of
H1 &
a = [x,y] )
by ZFMISC_1:def 2;
consider x1,
y1 being
set such that A38:
(
x1 in the
carrier of
H1 &
y1 in the
carrier of
H1 &
a = [x1,y1] )
by A31, ZFMISC_1:def 2;
(
x = x1 &
y = y1 )
by A37, A38, ZFMISC_1:33;
then
the
carrier of
H1 /\ the
carrier of
H2 <> {}
by A37, A38, XBOOLE_0:def 4;
hence
a in the
InternalRel of
H1
by A1, XBOOLE_0:def 7;
:: thesis: verum end;
end;
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
let a be
set ;
:: 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
a in the
InternalRel of
G |_2 the
carrier of
H2
;
:: thesis: a in the InternalRel of H2
then A40:
(
a in the
InternalRel of
G &
a in [:the carrier of H2,the carrier of H2:] )
by 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 A41:
(
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 A41, XBOOLE_0:def 3;
suppose
a in the
InternalRel of
H1
;
:: thesis: a in the InternalRel of H2then consider x,
y being
set such that A42:
(
a = [x,y] &
x in the
carrier of
H1 &
y in the
carrier of
H1 )
by RELSET_1:6;
consider x1,
y1 being
set such that A43:
(
x1 in the
carrier of
H2 &
y1 in the
carrier of
H2 &
a = [x1,y1] )
by A40, ZFMISC_1:def 2;
(
x = x1 &
y = y1 )
by A42, A43, ZFMISC_1:33;
then
the
carrier of
H1 /\ the
carrier of
H2 <> {}
by A42, A43, XBOOLE_0:def 4;
hence
a in the
InternalRel of
H2
by A1, XBOOLE_0:def 7;
:: thesis: verum end; suppose
a in [:the carrier of H1,the carrier of H2:]
;
:: thesis: a in the InternalRel of H2then consider x,
y being
set such that A44:
(
x in the
carrier of
H1 &
y in the
carrier of
H2 &
a = [x,y] )
by ZFMISC_1:def 2;
consider x1,
y1 being
set such that A45:
(
x1 in the
carrier of
H2 &
y1 in the
carrier of
H2 &
a = [x1,y1] )
by A40, ZFMISC_1:def 2;
(
x = x1 &
y = y1 )
by A44, A45, ZFMISC_1:33;
then
the
carrier of
H1 /\ the
carrier of
H2 <> {}
by A44, A45, XBOOLE_0:def 4;
hence
a in the
InternalRel of
H2
by A1, XBOOLE_0:def 7;
:: thesis: verum end; suppose
a in [:the carrier of H2,the carrier of H1:]
;
:: thesis: a in the InternalRel of H2then consider x,
y being
set such that A46:
(
x in the
carrier of
H2 &
y in the
carrier of
H1 &
a = [x,y] )
by ZFMISC_1:def 2;
consider x1,
y1 being
set such that A47:
(
x1 in the
carrier of
H2 &
y1 in the
carrier of
H2 &
a = [x1,y1] )
by A40, ZFMISC_1:def 2;
(
x = x1 &
y = y1 )
by A46, A47, ZFMISC_1:33;
then
the
carrier of
H1 /\ the
carrier of
H2 <> {}
by A46, A47, XBOOLE_0:def 4;
hence
a in the
InternalRel of
H2
by A1, XBOOLE_0:def 7;
:: thesis: verum end;
end; hence
(
H1 is
full SubRelStr of
G &
H2 is
full SubRelStr of
G )
by A22, A24, A26, A27, A28, A29, YELLOW_0:def 13, YELLOW_0:def 14;
:: thesis: verum end;