let S be SubSpace of T; :: thesis: 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; :: according to PRE_TOPC:def 1 :: thesis: ( ( 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 :: thesis: 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

proof

let a be Subset-Family of S; :: thesis: ( a c= the topology of S implies union a in the topology of S )
assume A3: a c= the topology of S ; :: thesis: union a in the topology of S
defpred S₁[ set ] means ( T /\ the carrier of S in a & T in the topology of T );
consider b being Subset-Family of T such that
A4: for Z being Subset of T holds
( Z in b iff S₁[Z] ) from SUBSET_1:sch 3();
A5: (union b) /\ the carrier of S c= union a

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (union b) /\ the carrier of S or x in union a )
assume A6: x in (union b) /\ the carrier of S ; :: thesis: x in union a
then x in union b by XBOOLE_0:def 4;
then consider Z being set such that
A7: x in Z and
A8: Z in b by TARSKI:def 4;
x in the carrier of S by A6, XBOOLE_0:def 4;
then A9: x in Z /\ the carrier of S by A7, XBOOLE_0:def 4;
Z /\ the carrier of S in a by A4, A8;
hence x in union a by A9, TARSKI:def 4; :: thesis: verum

end;

b c= the topology of T by A4;
then A10: union b in the topology of T by Def1;
union a c= (union b) /\ the carrier of S

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union a or x in (union b) /\ the carrier of S )
assume A11: x in union a ; :: thesis: x in (union b) /\ the carrier of S
then consider Z1 being set such that
A12: x in Z1 and
A13: Z1 in a by TARSKI:def 4;
consider Z3 being Subset of T such that
A14: ( Z3 in the topology of T & Z1 = Z3 /\ the carrier of S ) by A2, A3, A13, Def4;
( Z3 in b & x in Z3 ) by A4, A12, A13, A14, XBOOLE_0:def 4;
then x in union b by TARSKI:def 4;
hence x in (union b) /\ the carrier of S by A11, XBOOLE_0:def 4; :: thesis: verum

end;

then union a = (union b) /\ the carrier of S by A5, XBOOLE_0:def 10;
hence union a in the topology of S by A2, A10, Def4; :: thesis: verum

end;

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 :: thesis: verum

proof

let V, Q be Subset of S; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum

end;

end;

hence S is TopSpace-like ; :: thesis: verum