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