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