take S = 1-sorted(# { the real-valued Function} #); :: thesis: ( S is strict & not S is empty & S is real-functions-membered )
thus S is strict ; :: thesis: ( not S is empty & S is real-functions-membered )
thus not the carrier of S is empty ; :: according to STRUCT_0:def 1 :: thesis: S is real-functions-membered
let x be object ; :: according to VALUED_2:def 4,TOPREALC:def 2 :: thesis: ( not x in the carrier of S or x is set )
thus ( not x in the carrier of S or x is set ) ; :: thesis: verum