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
now :: thesis: for G being Subset of Y st G is open & B meets G holds
B 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;
hence B is anti-discrete ; :: thesis: verum