set IT = { r where r is Real : r >= 0 } ;

now

let x be set ; :: thesis: ( x in { r where r is Real : r >= 0 } implies x in REAL )
assume x in { r where r is Real : r >= 0 } ; :: thesis: x in REAL
then ex r being Real st
( x = r & r >= 0 ) ;
hence x in REAL ; :: thesis: verum

end;

hence { r where r is Real : r >= 0 } is Subset of REAL by TARSKI:def 3; :: thesis: verum