now

take X = {{} }; :: thesis: ex T being Subset-Family of X st
( the carrier of TopStruct(# X,T #) in the topology of TopStruct(# X,T #) & ( for a being Subset-Family of TopStruct(# X,T #) st a c= the topology of TopStruct(# X,T #) holds
union a in the topology of TopStruct(# X,T #) ) & ( for a, b being Subset of TopStruct(# X,T #) st a in the topology of TopStruct(# X,T #) & b in the topology of TopStruct(# X,T #) holds
a /\ b in the topology of TopStruct(# X,T #) ) )
set T = {{} ,X};
{{} ,X} c= bool X

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {{} ,X} or x in bool X )
assume x in {{} ,X} ; :: thesis: x in bool X
then ( x = {} or x = X ) by TARSKI:def 2;
then x c= X by XBOOLE_1:2;
hence x in bool X ; :: thesis: verum

end;

then reconsider T = {{} ,X} as Subset-Family of X ;
take T = T; :: thesis: ( the carrier of TopStruct(# X,T #) in the topology of TopStruct(# X,T #) & ( for a being Subset-Family of TopStruct(# X,T #) st a c= the topology of TopStruct(# X,T #) holds
union a in the topology of TopStruct(# X,T #) ) & ( for a, b being Subset of TopStruct(# X,T #) st a in the topology of TopStruct(# X,T #) & b in the topology of TopStruct(# X,T #) holds
a /\ b in the topology of TopStruct(# X,T #) ) )
set Y = TopStruct(# X,T #);
thus the carrier of TopStruct(# X,T #) in the topology of TopStruct(# X,T #) by TARSKI:def 2; :: thesis: ( ( for a being Subset-Family of TopStruct(# X,T #) st a c= the topology of TopStruct(# X,T #) holds
union a in the topology of TopStruct(# X,T #) ) & ( for a, b being Subset of TopStruct(# X,T #) st a in the topology of TopStruct(# X,T #) & b in the topology of TopStruct(# X,T #) holds
a /\ b in the topology of TopStruct(# X,T #) ) )
thus for a being Subset-Family of TopStruct(# X,T #) st a c= the topology of TopStruct(# X,T #) holds
union a in the topology of TopStruct(# X,T #) :: thesis: for a, b being Subset of TopStruct(# X,T #) st a in the topology of TopStruct(# X,T #) & b in the topology of TopStruct(# X,T #) holds
a /\ b in the topology of TopStruct(# X,T #)

proof

let a be Subset-Family of TopStruct(# X,T #); :: thesis: ( a c= the topology of TopStruct(# X,T #) implies union a in the topology of TopStruct(# X,T #) )
assume a c= the topology of TopStruct(# X,T #) ; :: thesis: union a in the topology of TopStruct(# X,T #)
then ( a = {} or a = {{} } or a = {X} or a = {{} ,X} ) by ZFMISC_1:42;
then ( union a = {} or union a = X or union a = {} \/ X ) by ZFMISC_1:2, ZFMISC_1:31, ZFMISC_1:93;
hence union a in the topology of TopStruct(# X,T #) by TARSKI:def 2; :: thesis: verum

end;

let a, b be Subset of TopStruct(# X,T #); :: thesis: ( a in the topology of TopStruct(# X,T #) & b in the topology of TopStruct(# X,T #) implies a /\ b in the topology of TopStruct(# X,T #) )
assume that
A1: a in the topology of TopStruct(# X,T #) and
A2: b in the topology of TopStruct(# X,T #) ; :: thesis: a /\ b in the topology of TopStruct(# X,T #)
( ( a = {} or a = X ) & ( b = {} or b = X ) ) by A1, A2, TARSKI:def 2;
hence a /\ b in the topology of TopStruct(# X,T #) by TARSKI:def 2; :: thesis: verum

end;

then consider X being non empty set , T being Subset-Family of X such that
A3: ( the carrier of TopStruct(# X,T #) in the topology of TopStruct(# X,T #) & ( for a being Subset-Family of TopStruct(# X,T #) st a c= the topology of TopStruct(# X,T #) holds
union a in the topology of TopStruct(# X,T #) ) & ( for a, b being Subset of TopStruct(# X,T #) st a in the topology of TopStruct(# X,T #) & b in the topology of TopStruct(# X,T #) holds
a /\ b in the topology of TopStruct(# X,T #) ) ) ;
take TopStruct(# X,T #) ; :: thesis: ( not TopStruct(# X,T #) is empty & TopStruct(# X,T #) is strict & TopStruct(# X,T #) is TopSpace-like )
thus not TopStruct(# X,T #) is empty ; :: thesis: ( TopStruct(# X,T #) is strict & TopStruct(# X,T #) is TopSpace-like )
thus ( TopStruct(# X,T #) is strict & TopStruct(# X,T #) is TopSpace-like ) by A3, Def1; :: thesis: verum