let Y be non empty TopStruct ; :: thesis: for A, B being Subset of Y st B c= A & A is anti-discrete holds

B is anti-discrete

let A, B be Subset of Y; :: thesis: ( B c= A & A is anti-discrete implies B is anti-discrete )

assume A1: B c= A ; :: thesis: ( not A is anti-discrete or B is anti-discrete )

assume A2: A is anti-discrete ; :: thesis: B is anti-discrete

B is anti-discrete

let A, B be Subset of Y; :: thesis: ( B c= A & A is anti-discrete implies B is anti-discrete )

assume A1: B c= A ; :: thesis: ( not A is anti-discrete or B is anti-discrete )

assume A2: A is anti-discrete ; :: thesis: B is anti-discrete

now :: thesis: for G being Subset of Y st G is open & B meets G holds

B c= G

hence
B is anti-discrete
; :: thesis: verumB c= G

let G be Subset of Y; :: thesis: ( G is open & B meets G implies B c= G )

assume A3: G is open ; :: thesis: ( B meets G implies B c= G )

assume B meets G ; :: thesis: B c= G

then B /\ G <> {} ;

then A /\ G <> {} by A1, XBOOLE_1:3, XBOOLE_1:26;

then A meets G ;

then A c= G by A2, A3;

hence B c= G by A1; :: thesis: verum

end;assume A3: G is open ; :: thesis: ( B meets G implies B c= G )

assume B meets G ; :: thesis: B c= G

then B /\ G <> {} ;

then A /\ G <> {} by A1, XBOOLE_1:3, XBOOLE_1:26;

then A meets G ;

then A c= G by A2, A3;

hence B c= G by A1; :: thesis: verum