now :: thesis: ex X being set 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 #) ) )
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 object ; :: according to TARSKI:def 3 :: thesis: ( not x in {{},X} or x in bool X )
reconsider xx = x as set by TARSKI:1;
assume x in {{},X} ; :: thesis: x in bool X
then ( x = {} or x = X ) by TARSKI:def 2;
then xx c= X ;
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:36;
then ( union a = {} or union a = X or union a = {} \/ X ) by ZFMISC_1:2, ZFMISC_1:25, ZFMISC_1:75;
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 #)
A3: ( b = {} or b = X ) by A2, TARSKI:def 2;
( a = {} or a = X ) by A1, TARSKI:def 2;
hence a /\ b in the topology of TopStruct(# X,T #) by A3, TARSKI:def 2; :: thesis: verum
end;
then consider X being non empty set , T being Subset-Family of X such that
A4: ( 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 A4; :: thesis: verum