( not bool X is empty & bool X is preBoolean ) ;
hence ex b₁ being Subset-Family of X st
( not b₁ is empty & b₁ is preBoolean ) ; :: thesis: verum