set A = { |[x,y]| where x, y is Real : y >= 0 } ;
{ |[x,y]| where x, y is Real : y >= 0 } c= the carrier of (TOP-REAL 2)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { |[x,y]| where x, y is Real : y >= 0 } or a in the carrier of (TOP-REAL 2) )
assume a in { |[x,y]| where x, y is Real : y >= 0 } ; :: thesis: a in the carrier of (TOP-REAL 2)
then ex x, y being Real st
( a = |[x,y]| & y >= 0 ) ;
hence a in the carrier of (TOP-REAL 2) ; :: thesis: verum

end;

hence { |[x,y]| where x, y is Real : y >= 0 } is Subset of (TOP-REAL 2) ; :: thesis: verum