let T be non empty TopSpace; :: thesis: for S being non empty SubSpace of T holds Omega S is full SubRelStr of Omega T
let S be non empty SubSpace of T; :: thesis: Omega S is full SubRelStr of Omega T
A1:
the carrier of S c= the carrier of T
by BORSUK_1:35;
A2:
the carrier of (Omega S) = the carrier of S
by Lm1;
then A3:
the carrier of (Omega S) c= the carrier of (Omega T)
by A1, Lm1;
A4:
the InternalRel of (Omega S) c= the InternalRel of (Omega T)
proof
let x,
y be
set ;
:: according to RELAT_1:def 3 :: thesis: ( not [x,y] in the InternalRel of (Omega S) or [x,y] in the InternalRel of (Omega T) )
assume A5:
[x,y] in the
InternalRel of
(Omega S)
;
:: thesis: [x,y] in the InternalRel of (Omega T)
then A6:
(
x in the
carrier of
(Omega S) &
y in the
carrier of
(Omega S) )
by ZFMISC_1:106;
reconsider o1 =
x,
o2 =
y as
Element of
(Omega S) by A5, ZFMISC_1:106;
o1 <= o2
by A5, ORDERS_2:def 9;
then consider Y2 being
Subset of
S such that A7:
Y2 = {o2}
and A8:
o1 in Cl Y2
by Def2;
reconsider s2 =
y as
Element of
S by A6, Lm1;
reconsider t2 =
y as
Element of
T by A1, A2, A6;
Cl {s2} = (Cl {t2}) /\ ([#] S)
by PRE_TOPC:47;
then A9:
Cl {s2} c= Cl {t2}
by XBOOLE_1:17;
reconsider o3 =
x,
o4 =
y as
Element of
(Omega T) by A1, A2, A6, Lm1;
o3 <= o4
by A7, A8, A9, Def2;
hence
[x,y] in the
InternalRel of
(Omega T)
by ORDERS_2:def 9;
:: thesis: verum
end;
the InternalRel of (Omega S) = the InternalRel of (Omega T) |_2 the carrier of (Omega S)
proof
let x,
y be
set ;
:: according to RELAT_1:def 2 :: thesis: ( ( not [x,y] in the InternalRel of (Omega S) or [x,y] in the InternalRel of (Omega T) |_2 the carrier of (Omega S) ) & ( not [x,y] in the InternalRel of (Omega T) |_2 the carrier of (Omega S) or [x,y] in the InternalRel of (Omega S) ) )
thus
(
[x,y] in the
InternalRel of
(Omega S) implies
[x,y] in the
InternalRel of
(Omega T) |_2 the
carrier of
(Omega S) )
by A4, XBOOLE_0:def 4;
:: thesis: ( not [x,y] in the InternalRel of (Omega T) |_2 the carrier of (Omega S) or [x,y] in the InternalRel of (Omega S) )
assume A10:
[x,y] in the
InternalRel of
(Omega T) |_2 the
carrier of
(Omega S)
;
:: thesis: [x,y] in the InternalRel of (Omega S)
then A11:
[x,y] in the
InternalRel of
(Omega T)
by XBOOLE_0:def 4;
A12:
(
x in the
carrier of
(Omega S) &
y in the
carrier of
(Omega S) )
by A10, ZFMISC_1:106;
reconsider o3 =
x,
o4 =
y as
Element of
(Omega S) by A10, ZFMISC_1:106;
reconsider s1 =
x,
s2 =
y as
Element of
S by A12, Lm1;
reconsider t1 =
x,
t2 =
y as
Element of
T by A1, A2, A12;
reconsider o1 =
x,
o2 =
y as
Element of
(Omega T) by A1, A2, A12, Lm1;
o1 <= o2
by A11, ORDERS_2:def 9;
then consider Y being
Subset of
T such that A13:
Y = {t2}
and A14:
t1 in Cl Y
by Def2;
Cl {s2} = (Cl {t2}) /\ ([#] S)
by PRE_TOPC:47;
then
s1 in Cl {s2}
by A13, A14, XBOOLE_0:def 4;
then
o3 <= o4
by Def2;
hence
[x,y] in the
InternalRel of
(Omega S)
by ORDERS_2:def 9;
:: thesis: verum
end;
hence
Omega S is full SubRelStr of Omega T
by A3, A4, YELLOW_0:def 13, YELLOW_0:def 14; :: thesis: verum