set x = the Element of X;

A1: now :: thesis: for x being object st x in { ||.(u . t).|| where t is Element of X : verum } holds
x in REAL

let x be object ; :: thesis: ( x in { ||.(u . t).|| where t is Element of X : verum } implies x in REAL )

now :: thesis: ( x in { ||.(u . t).|| where t is Element of X : verum } implies x in REAL )

assume x in { ||.(u . t).|| where t is Element of X : verum } ; :: thesis: x in REAL
then ex t being Element of X st x = ||.(u . t).|| ;
hence x in REAL ; :: thesis: verum

end;

hence ( x in { ||.(u . t).|| where t is Element of X : verum } implies x in REAL ) ; :: thesis: verum

end;

||.(u . the Element of X).|| in { ||.(u . t).|| where t is Element of X : verum } ;
hence { ||.(u . t).|| where t is Element of X : verum } is non empty Subset of REAL by A1, TARSKI:def 3; :: thesis: verum