consider D being non empty set , Z being Element of D, a being BinOp of D, m being Function of [:REAL,D:],D, s being Function of [:D,D:],REAL;
take UNITSTR(# D,Z,a,m,s #) ; :: thesis: ( not UNITSTR(# D,Z,a,m,s #) is empty & UNITSTR(# D,Z,a,m,s #) is strict )
thus not the carrier of UNITSTR(# D,Z,a,m,s #) is empty ; :: according to STRUCT_0:def 1 :: thesis: UNITSTR(# D,Z,a,m,s #) is strict
thus UNITSTR(# D,Z,a,m,s #) is strict ; :: thesis: verum