hereby :: thesis: ( ( for D being Subset of Y st D c= A holds
ex F being Subset of Y st
( F is closed & A /\ F = D ) ) implies A is discrete )

assume A1: A is discrete ; :: thesis: for D being Subset of Y st D c= A holds
ex F being Subset of Y st
( F is closed & A /\ F = D )
let D be Subset of Y; :: thesis: ( D c= A implies ex F being Subset of Y st
( F is closed & A /\ F = D ) )
A \ D c= A by XBOOLE_1:36;
then consider G being Subset of Y such that
A2: G is open and
A3: A /\ G = A \ D by A1, Def5;
assume A4: D c= A ; :: thesis: ex F being Subset of Y st
( F is closed & A /\ F = D )

now

take F = ([#] Y) \ G; :: thesis: ( F is closed & A /\ F = D )
G = ([#] Y) \ F by PRE_TOPC:3;
hence F is closed by A2, PRE_TOPC:def 3; :: thesis: A /\ F = D
A /\ ([#] Y) = A by XBOOLE_1:28;
then A /\ F = A \ G by XBOOLE_1:49;
then A /\ F = A \ (A \ D) by A3, XBOOLE_1:47;
then A /\ F = A /\ D by XBOOLE_1:48;
hence A /\ F = D by A4, XBOOLE_1:28; :: thesis: verum

end;

hence ex F being Subset of Y st
( F is closed & A /\ F = D ) ; :: thesis: verum

end;

hereby :: thesis: verum

assume A5: for D being Subset of Y st D c= A holds
ex F being Subset of Y st
( F is closed & A /\ F = D ) ; :: thesis: A is discrete

now

let D be Subset of Y; :: thesis: ( D c= A implies ex G being Subset of Y st
( G is open & A /\ G = D ) )
consider F being Subset of Y such that
A6: F is closed and
A7: A /\ F = A \ D by A5, XBOOLE_1:36;
assume A8: D c= A ; :: thesis: ex G being Subset of Y st
( G is open & A /\ G = D )

now

take G = ([#] Y) \ F; :: thesis: ( G is open & A /\ G = D )
thus G is open by A6, PRE_TOPC:def 3; :: thesis: A /\ G = D
A /\ ([#] Y) = A by XBOOLE_1:28;
then A /\ G = A \ F by XBOOLE_1:49;
then A /\ G = A \ (A \ D) by A7, XBOOLE_1:47;
then A /\ G = A /\ D by XBOOLE_1:48;
hence A /\ G = D by A8, XBOOLE_1:28; :: thesis: verum

end;

hence ex G being Subset of Y st
( G is open & A /\ G = D ) ; :: thesis: verum

end;

hence A is discrete by Def5; :: thesis: verum

end;