let X be set ; :: thesis: ( X is empty implies X is Relation-like )
assume X is empty ; :: thesis: X is Relation-like
hence for p being set st p in X holds
ex x, y being set st [x,y] = p ; :: according to RELAT_1:def 1 :: thesis: verum