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