let T be TopStruct ; :: thesis: for A being Subset of T st A <> {} T holds
ex x being Point of T st x in A
let A be Subset of T; :: thesis: ( A <> {} T implies ex x being Point of T st x in A )
set x = the Element of A;
assume A1: A <> {} T ; :: thesis: ex x being Point of T st x in A
then the Element of A is Point of T by TARSKI:def 3;
hence ex x being Point of T st x in A by A1; :: thesis: verum