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

proof

hence
{ nl where nl is Liouville : verum } is Subset of REAL
; :: thesis: verum
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;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