let S be SubSpace of T; S is TopSpace-like
S is TopSpace-like
proof
set P = the
carrier of
S;
A1:
[#] T in the
topology of
T
by Def1;
A2:
the
carrier of
S = [#] S
;
then
the
carrier of
S c= [#] T
by Def4;
then
([#] T) /\ the
carrier of
S = the
carrier of
S
by XBOOLE_1:28;
hence
the
carrier of
S in the
topology of
S
by A2, A1, Def4;
PRE_TOPC:def 1 ( ( for a being Subset-Family of S st a c= the topology of S holds
union a in the topology of S ) & ( for a, b being Subset of S st a in the topology of S & b in the topology of S holds
a /\ b in the topology of S ) )
thus
for
a being
Subset-Family of
S st
a c= the
topology of
S holds
union a in the
topology of
S
for a, b being Subset of S st a in the topology of S & b in the topology of S holds
a /\ b in the topology of S
thus
for
V,
Q being
Subset of
S st
V in the
topology of
S &
Q in the
topology of
S holds
V /\ Q in the
topology of
S
verumproof
let V,
Q be
Subset of
S;
( V in the topology of S & Q in the topology of S implies V /\ Q in the topology of S )
assume that A15:
V in the
topology of
S
and A16:
Q in the
topology of
S
;
V /\ Q in the topology of S
consider P1 being
Subset of
T such that A17:
P1 in the
topology of
T
and A18:
V = P1 /\ the
carrier of
S
by A2, A15, Def4;
consider Q1 being
Subset of
T such that A19:
Q1 in the
topology of
T
and A20:
Q = Q1 /\ the
carrier of
S
by A2, A16, Def4;
A21:
V /\ Q =
P1 /\ ((Q1 /\ the carrier of S) /\ the carrier of S)
by A18, A20, XBOOLE_1:16
.=
P1 /\ (Q1 /\ ( the carrier of S /\ the carrier of S))
by XBOOLE_1:16
.=
(P1 /\ Q1) /\ the
carrier of
S
by XBOOLE_1:16
;
P1 /\ Q1 in the
topology of
T
by A17, A19, Def1;
hence
V /\ Q in the
topology of
S
by A2, A21, Def4;
verum
end;
end;
hence
S is TopSpace-like
; verum