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