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 consider r being Real such that
A1: ( x = r & r >= 0 ) ;
thus x in REAL by A1; :: thesis: verum

end;

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