consider D being non empty set , f being Relation of D;
take RelStr(# D,f #) ; :: thesis: ( not RelStr(# D,f #) is empty & RelStr(# D,f #) is strict )
thus not the carrier of RelStr(# D,f #) is empty ; :: according to STRUCT_0:def 1 :: thesis: RelStr(# D,f #) is strict
thus RelStr(# D,f #) is strict ; :: thesis: verum