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

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

assume A is T_0 ; :: thesis: Y0 is T_0
then for x, y being Point of Y st x is Point of Y0 & y is Point of Y0 & x <> y & ( for E being Subset of Y holds
( not E is closed or not x in E or y in E ) ) holds
ex F being Subset of Y st
( F is closed & not x in F & y in F ) by A1, Def9;
hence Y0 is T_0 by Def14; :: thesis: verum

end;

hereby :: thesis: verum

assume Y0 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 E being Subset of Y holds
( not E is closed or not x in E or y in E ) ) holds
ex F being Subset of Y st
( F is closed & not x in F & y in F ) by A1, Def14;
hence A is T_0 by Def9; :: thesis: verum

end;