let Y be non empty TopStruct ; :: thesis: for A, B being Subset of Y st B c= A & A is T_0 holds
B is T_0
let A, B be Subset of Y; :: thesis: ( B c= A & A is T_0 implies B is T_0 )
assume A1: B c= A ; :: thesis: ( not A is T_0 or B is T_0 )
assume A is T_0 ; :: thesis: B is T_0
then for x, y being Point of Y st x in B & y in B & 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 A1, Def8;
hence B is T_0 by Def8; :: thesis: verum