set X = the non empty set ;
set F = the Function of [: the non empty set , the non empty set :],REAL;
set O = the Element of the non empty set ;
set B = the BinOp of the non empty set ;
set G = the Function of [:REAL, the non empty set :], the non empty set ;
take
RLSMetrStruct(# the non empty set , the Function of [: the non empty set , the non empty set :],REAL, the Element of the non empty set , the BinOp of the non empty set , the Function of [:REAL, the non empty set :], the non empty set #)
; ( not RLSMetrStruct(# the non empty set , the Function of [: the non empty set , the non empty set :],REAL, the Element of the non empty set , the BinOp of the non empty set , the Function of [:REAL, the non empty set :], the non empty set #) is empty & RLSMetrStruct(# the non empty set , the Function of [: the non empty set , the non empty set :],REAL, the Element of the non empty set , the BinOp of the non empty set , the Function of [:REAL, the non empty set :], the non empty set #) is strict )
thus
not the carrier of RLSMetrStruct(# the non empty set , the Function of [: the non empty set , the non empty set :],REAL, the Element of the non empty set , the BinOp of the non empty set , the Function of [:REAL, the non empty set :], the non empty set #) is empty
; STRUCT_0:def 1 RLSMetrStruct(# the non empty set , the Function of [: the non empty set , the non empty set :],REAL, the Element of the non empty set , the BinOp of the non empty set , the Function of [:REAL, the non empty set :], the non empty set #) is strict
thus
RLSMetrStruct(# the non empty set , the Function of [: the non empty set , the non empty set :],REAL, the Element of the non empty set , the BinOp of the non empty set , the Function of [:REAL, the non empty set :], the non empty set #) is strict
; verum