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

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