take {} ; :: thesis: ( {} is empty & {} is I -defined & {} is f -compatible )
thus ( {} is empty & {} is I -defined & {} is f -compatible ) by RELAT_1:171; :: thesis: verum