take R = RelStr(# {}, the Relation of {} #); :: thesis: ( R is strict & R is empty )
thus R is strict ; :: thesis: R is empty
thus the carrier of R is empty ; :: according to STRUCT_0:def 1 :: thesis: verum