reconsider a = {0} as finite Subset of REAL ;
take a ; :: thesis: ( not a is empty & a is finite & a is bounded )
thus ( not a is empty & a is finite & a is bounded ) ; :: thesis: verum