{ nl where nl is Liouville : verum } c= REAL

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { nl where nl is Liouville : verum } or x in REAL )
assume x in { nl where nl is Liouville : verum } ; :: thesis: x in REAL
then ex nl being Liouville st x = nl ;
hence x in REAL by XREAL_0:def 1; :: thesis: verum

end;

hence { nl where nl is Liouville : verum } is Subset of REAL ; :: thesis: verum