{} in sproduct f by Th50;
hence ex b₁ being Element of sproduct f st b₁ is empty ; :: thesis: verum