let X be non empty TopSpace; :: thesis: for Y0 being non empty SubSpace of X st ( for X0 being closed SubSpace of X holds
( Y0 misses X0 or Y0 is SubSpace of X0 ) ) holds
Y0 is anti-discrete
let Y0 be non empty SubSpace of X; :: thesis: ( ( for X0 being closed SubSpace of X holds
( Y0 misses X0 or Y0 is SubSpace of X0 ) ) implies Y0 is anti-discrete )
reconsider A = the carrier of Y0 as Subset of X by TSEP_1:1;
assume A1: for X0 being closed SubSpace of X holds
( Y0 misses X0 or Y0 is SubSpace of X0 ) ; :: thesis: Y0 is anti-discrete
now :: thesis: for G being Subset of X holds
( not G is closed or A misses G or A c= G )
let G be Subset of X; :: thesis: ( not G is closed or A misses G or A c= G )
assume A2: G is closed ; :: thesis: ( A misses G or A c= G )
now :: thesis: ( A misses G or A c= G )
per cases ( G is empty or not G is empty ) ;
suppose G is empty ; :: thesis: ( A misses G or A c= G )
hence ( A misses G or A c= G ) ; :: thesis: verum
end;
suppose not G is empty ; :: thesis: ( A misses G or A c= G )
then consider X0 being non empty strict closed SubSpace of X such that
A3: G = the carrier of X0 by A2, TSEP_1:15;
( Y0 misses X0 or Y0 is SubSpace of X0 ) by A1;
hence ( A misses G or A c= G ) by A3, TSEP_1:4, TSEP_1:def 3; :: thesis: verum
end;
end;
end;
hence ( A misses G or A c= G ) ; :: thesis: verum
end;
then A is anti-discrete ;
hence Y0 is anti-discrete by Th67; :: thesis: verum