{} is Relation of X,Y by XBOOLE_1:2;
hence ex b₁ being Relation of X,Y st b₁ is empty ; :: thesis: verum