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