set O1 = { U where U is Subset of X : not x0 in U } ;
set O2 = { (F `) where F is Subset of X : F is finite } ;
set O = { U where U is Subset of X : not x0 in U } \/ { (F `) where F is Subset of X : F is finite } ;
{ U where U is Subset of X : not x0 in U } \/ { (F `) where F is Subset of X : F is finite } c= bool X
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { U where U is Subset of X : not x0 in U } \/ { (F `) where F is Subset of X : F is finite } or a in bool X )
assume a in { U where U is Subset of X : not x0 in U } \/ { (F `) where F is Subset of X : F is finite } ; :: thesis: a in bool X
then ( a in { U where U is Subset of X : not x0 in U } or a in { (F `) where F is Subset of X : F is finite } ) by XBOOLE_0:def 3;
then ( ex U being Subset of X st
( a = U & not x0 in U ) or ex F being Subset of X st
( a = F ` & F is finite ) ) ;
hence a in bool X ; :: thesis: verum
end;
then reconsider O = { U where U is Subset of X : not x0 in U } \/ { (F `) where F is Subset of X : F is finite } as Subset-Family of X ;
take TopStruct(# X,O #) ; :: thesis: ( the carrier of TopStruct(# X,O #) = X & the topology of TopStruct(# X,O #) = { U where U is Subset of X : not x0 in U } \/ { (F `) where F is Subset of X : F is finite } )
thus ( the carrier of TopStruct(# X,O #) = X & the topology of TopStruct(# X,O #) = { U where U is Subset of X : not x0 in U } \/ { (F `) where F is Subset of X : F is finite } ) ; :: thesis: verum