take {} ; :: thesis: ( {} is non-empty & {} is I -defined )
thus {} is non-empty ; :: thesis: {} is I -defined
thus dom {} c= I ; :: according to RELAT_1:def 18 :: thesis: verum