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