let X be set ; :: thesis: ( X is empty implies X is relation-like )
assume X is empty ; :: thesis: X is relation-like
hence ( ( for x being set st x in X holds
x is FinSequence ) & ( for a, b being FinSequence st a in X & b in X holds
len a = len b ) ) ; :: according to MARGREL1:def 1 :: thesis: verum