{} is FinPartState of S by FUNCT_1:174, RELAT_1:206;
hence ex b₁ being FinPartState of S st b₁ is empty ; :: thesis: verum