{} is FinPartState of by CARD_3:66;
hence ex b₁ being FinPartState of st b₁ is empty ; :: thesis: verum