consider A being non empty set , r being Function of [:A,A:],REAL ;
take MetrStruct(# A,r #) ; :: thesis: ( not MetrStruct(# A,r #) is empty & MetrStruct(# A,r #) is strict )
thus not the carrier of MetrStruct(# A,r #) is empty ; :: according to STRUCT_0:def 1 :: thesis: MetrStruct(# A,r #) is strict
thus MetrStruct(# A,r #) is strict ; :: thesis: verum