let Y be non empty TopStruct ; :: thesis: for A being Subset of Y st A = the carrier of Y holds
( A is T_0 iff Y is T_0 )
let A be Subset of Y; :: thesis: ( A = the carrier of Y implies ( A is T_0 iff Y is T_0 ) )
assume A1: A = the carrier of Y ; :: thesis: ( A is T_0 iff Y is T_0 )

hereby :: thesis: ( Y is T_0 implies A is T_0 )

assume A is T_0 ; :: thesis: Y is T_0
then for x, y being Point of Y holds
( not x <> y or ex V being Subset of Y st
( V is open & x in V & not y in V ) or ex W being Subset of Y st
( W is open & not x in W & y in W ) ) by A1, Def8;
hence Y is T_0 by Def3; :: thesis: verum

end;

hereby :: thesis: verum

assume Y is T_0 ; :: thesis: A is T_0
then for x, y being Point of Y st x in A & y in A & x <> y & ( for V being Subset of Y holds
( not V is open or not x in V or y in V ) ) holds
ex W being Subset of Y st
( W is open & not x in W & y in W ) by Def3;
hence A is T_0 by Def8; :: thesis: verum

end;