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

hence Y0 is anti-discrete by Th67; :: thesis: verum

( 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 )

then
A is anti-discrete
;( 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 )

end;assume A2: G is closed ; :: thesis: ( A misses G or A c= G )

now :: thesis: ( A misses G or A c= G )end;

hence
( A misses G or A c= G )
; :: thesis: verumper cases
( G is empty or not G is empty )
;

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;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

hence Y0 is anti-discrete by Th67; :: thesis: verum