let Y be TopStruct ; :: thesis: for A, B being Subset of Y st B c= A & A is discrete holds
B is discrete
let A, B be Subset of Y; :: thesis: ( B c= A & A is discrete implies B is discrete )
assume A1: B c= A ; :: thesis: ( not A is discrete or B is discrete )
assume A2: A is discrete ; :: thesis: B is discrete

now :: thesis: for D being Subset of Y st D c= B holds
ex G being Subset of Y st
( G is open & B /\ G = D )

let D be Subset of Y; :: thesis: ( D c= B implies ex G being Subset of Y st
( G is open & B /\ G = D ) )
assume A3: D c= B ; :: thesis: ex G being Subset of Y st
( G is open & B /\ G = D )
then D c= A by A1, XBOOLE_1:1;
then consider G being Subset of Y such that
A4: G is open and
A5: A /\ G = D by A2;

hereby :: thesis: verum

take G = G; :: thesis: ( G is open & B /\ G = D )
D c= G by A5, XBOOLE_1:17;
then A6: D c= B /\ G by A3, XBOOLE_1:19;
B /\ G c= A /\ G by A1, XBOOLE_1:26;
hence ( G is open & B /\ G = D ) by A4, A5, A6; :: thesis: verum

end;

end;

hence B is discrete ; :: thesis: verum