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 ) by PRE_TOPC:def 2; :: thesis: ( ( for A being Subset of X holds A is open ) implies X is discrete )
assume for A being Subset of X holds A is open ; :: thesis: X is discrete
then for V being object holds
( V in the topology of X iff V in bool the carrier of X ) by PRE_TOPC:def 2;
then the topology of X = bool the carrier of X by TARSKI:2;
hence X is discrete ; :: thesis: verum