1 in Real>=0 ;
hence not Real>=0 is empty ; :: thesis: verum