let X be TopSpace; :: thesis: ( X is discrete iff for A being Subset of X holds A is open )
thus ( X is discrete implies for A being Subset of X holds A is open ) :: thesis: ( ( for A being Subset of X holds A is open ) implies X is discrete )

proof

assume A1: X is discrete ; :: thesis: for A being Subset of X holds A is open
let A be Subset of X; :: thesis: A is open
the topology of X = bool the carrier of X by A1, Def1;
hence A is open by PRE_TOPC:def 2; :: thesis: verum

end;

assume A2: for A being Subset of X holds A is open ; :: thesis: X is discrete
for V being set holds
( V in the topology of X iff V in bool the carrier of X )

proof

let V be set ; :: thesis: ( V in the topology of X iff V in bool the carrier of X )

now

assume V in bool the carrier of X ; :: thesis: V in the topology of X
then reconsider C = V as Subset of X ;
C is open by A2;
hence V in the topology of X by PRE_TOPC:def 2; :: thesis: verum

end;

hence ( V in the topology of X iff V in bool the carrier of X ) ; :: thesis: verum

end;

then the topology of X = bool the carrier of X by TARSKI:1;
hence X is discrete by Def1; :: thesis: verum