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

proof

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

end;

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