let T be non empty TopSpace; 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; Omega S is full SubRelStr of Omega T
A1:
the carrier of S c= the carrier of T
by BORSUK_1:1;
A2:
the carrier of (Omega S) = the carrier of S
by Lm1;
A3:
the InternalRel of (Omega S) c= the InternalRel of (Omega T)
proof
let x,
y be
object ;
RELAT_1:def 3 ( not [x,y] in the InternalRel of (Omega S) or [x,y] in the InternalRel of (Omega T) )
assume A4:
[x,y] in the
InternalRel of
(Omega S)
;
[x,y] in the InternalRel of (Omega T)
then reconsider o1 =
x,
o2 =
y as
Element of
(Omega S) by ZFMISC_1:87;
A5:
y in the
carrier of
(Omega S)
by A4, ZFMISC_1:87;
then reconsider s2 =
y as
Element of
S by Lm1;
x in the
carrier of
(Omega S)
by A4, ZFMISC_1:87;
then reconsider o3 =
x,
o4 =
y as
Element of
(Omega T) by A1, A2, A5, Lm1;
reconsider t2 =
y as
Element of
T by A1, A2, A5;
Cl {s2} = (Cl {t2}) /\ ([#] S)
by PRE_TOPC:17;
then A6:
Cl {s2} c= Cl {t2}
by XBOOLE_1:17;
o1 <= o2
by A4;
then
ex
Y2 being
Subset of
S st
(
Y2 = {o2} &
o1 in Cl Y2 )
by Def2;
then
o3 <= o4
by A6, Def2;
hence
[x,y] in the
InternalRel of
(Omega T)
;
verum
end;
A7:
the InternalRel of (Omega S) = the InternalRel of (Omega T) |_2 the carrier of (Omega S)
proof
let x,
y be
object ;
RELAT_1:def 2 ( ( 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 A3, XBOOLE_0:def 4;
( 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 A8:
[x,y] in the
InternalRel of
(Omega T) |_2 the
carrier of
(Omega S)
;
[x,y] in the InternalRel of (Omega S)
then A9:
y in the
carrier of
(Omega S)
by ZFMISC_1:87;
A10:
x in the
carrier of
(Omega S)
by A8, ZFMISC_1:87;
then reconsider t1 =
x,
t2 =
y as
Element of
T by A1, A2, A9;
reconsider o1 =
x,
o2 =
y as
Element of
(Omega T) by A1, A2, A10, A9, Lm1;
[x,y] in the
InternalRel of
(Omega T)
by A8, XBOOLE_0:def 4;
then
o1 <= o2
;
then A11:
ex
Y being
Subset of
T st
(
Y = {t2} &
t1 in Cl Y )
by Def2;
reconsider s1 =
x,
s2 =
y as
Element of
S by A10, A9, Lm1;
reconsider o3 =
x,
o4 =
y as
Element of
(Omega S) by A8, ZFMISC_1:87;
Cl {s2} = (Cl {t2}) /\ ([#] S)
by PRE_TOPC:17;
then
s1 in Cl {s2}
by A11, XBOOLE_0:def 4;
then
o3 <= o4
by Def2;
hence
[x,y] in the
InternalRel of
(Omega S)
;
verum
end;
the carrier of (Omega S) c= the carrier of (Omega T)
by A1, A2, Lm1;
hence
Omega S is full SubRelStr of Omega T
by A3, A7, YELLOW_0:def 13, YELLOW_0:def 14; verum