set A = { |.(x - x0).| where x0 is Element of REAL n : x0 in L } ;
{ |.(x - x0).| where x0 is Element of REAL n : x0 in L } c= REAL

proof

let r be object ; :: according to TARSKI:def 3 :: thesis: ( not r in { |.(x - x0).| where x0 is Element of REAL n : x0 in L } or r in REAL )
assume r in { |.(x - x0).| where x0 is Element of REAL n : x0 in L } ; :: thesis: r in REAL
then ex x0 being Element of REAL n st
( r = |.(x - x0).| & x0 in L ) ;
hence r in REAL by XREAL_0:def 1; :: thesis: verum

end;

hence { |.(x - x0).| where x0 is Element of REAL n : x0 in L } is Subset of REAL ; :: thesis: verum