let Y be non empty TopStruct ; :: thesis: for Y0 being non empty SubSpace of Y
for Y1 being non empty T_0 SubSpace of Y st Y0 is SubSpace of Y1 holds
Y0 is T_0
let Y0 be non empty SubSpace of Y; :: thesis: for Y1 being non empty T_0 SubSpace of Y st Y0 is SubSpace of Y1 holds
Y0 is T_0
let Y1 be non empty T_0 SubSpace of Y; :: thesis: ( Y0 is SubSpace of Y1 implies Y0 is T_0 )
reconsider A1 = the carrier of Y1, A0 = the carrier of Y0 as non empty Subset of Y by Lm3;
assume A1: Y0 is SubSpace of Y1 ; :: thesis: Y0 is T_0
A2: A1 is T_0 by Th13;
( [#] Y0 = A0 & [#] Y1 = A1 ) ;
then A0 c= A1 by A1, PRE_TOPC:def 4;
then A0 is T_0 by A2;
hence Y0 is T_0 ; :: thesis: verum