reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
thus ( X0 is maximal_T_0 implies ( X0 is V59() & ( for Y0 being non empty V59() SubSpace of X st X0 is SubSpace of Y0 holds
TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of Y0, the topology of Y0 #) ) ) ) :: thesis: ( X0 is V59() & ( for Y0 being non empty V59() SubSpace of X st X0 is SubSpace of Y0 holds
TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of Y0, the topology of Y0 #) ) implies X0 is maximal_T_0 )
proof
assume X0 is maximal_T_0 ; :: thesis: ( X0 is V59() & ( for Y0 being non empty V59() SubSpace of X st X0 is SubSpace of Y0 holds
TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of Y0, the topology of Y0 #) ) )
then A1: A is maximal_T_0 ;
then A is T_0 ;
hence X0 is V59() by TSP_1:13; :: thesis: for Y0 being non empty V59() SubSpace of X st X0 is SubSpace of Y0 holds
TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of Y0, the topology of Y0 #)
thus for Y0 being non empty V59() SubSpace of X st X0 is SubSpace of Y0 holds
TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of Y0, the topology of Y0 #) :: thesis: verum
proof
let Y0 be non empty V59() SubSpace of X; :: thesis: ( X0 is SubSpace of Y0 implies TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of Y0, the topology of Y0 #) )
reconsider D = the carrier of Y0 as Subset of X by TSEP_1:1;
assume X0 is SubSpace of Y0 ; :: thesis: TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of Y0, the topology of Y0 #)
then A2: A c= D by TSEP_1:4;
D is T_0 by TSP_1:13;
then A = D by A1, A2;
hence TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of Y0, the topology of Y0 #) by TSEP_1:5; :: thesis: verum
end;
end;
assume X0 is V59() ; :: thesis: ( ex Y0 being non empty V59() SubSpace of X st
( X0 is SubSpace of Y0 & not TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of Y0, the topology of Y0 #) ) or X0 is maximal_T_0 )
then A3: A is T_0 by TSP_1:13;
assume A4: for Y0 being non empty V59() SubSpace of X st X0 is SubSpace of Y0 holds
TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of Y0, the topology of Y0 #) ; :: thesis: X0 is maximal_T_0
now :: thesis: for D being Subset of X st D is T_0 & A c= D holds
A = D
let D be Subset of X; :: thesis: ( D is T_0 & A c= D implies A = D )
assume A5: D is T_0 ; :: thesis: ( A c= D implies A = D )
assume A6: A c= D ; :: thesis: A = D
then D <> {} ;
then consider Y0 being non empty strict V59() SubSpace of X such that
A7: D = the carrier of Y0 by A5, TSP_1:18;
X0 is SubSpace of Y0 by A6, A7, TSEP_1:4;
hence A = D by A4, A7; :: thesis: verum
end;
then A is maximal_T_0 by A3;
hence X0 is maximal_T_0 ; :: thesis: verum