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;
assume A4: D c= A ; :: thesis: ex F being Subset of Y st
( F is closed & A /\ F = D )
now :: thesis: ex F being Element of bool the carrier of Y st
( F is closed & A /\ F = D )
take F = ([#] Y) \ G; :: thesis: ( F is closed & A /\ F = D )
G = ([#] Y) \ F by PRE_TOPC:3;
hence F is closed by A2; :: 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 :: thesis: for D being Subset of Y st D c= A holds
ex G being Subset of Y st
( G is open & A /\ G = D )
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 :: thesis: ex G being Element of bool the carrier of Y st
( G is open & A /\ G = D )
take G = ([#] Y) \ F; :: thesis: ( G is open & A /\ G = D )
thus G is open by A6; :: 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 ; :: thesis: verum
end;