{} is Event of Si by Th4;
hence ex b₁ being Event of Si st b₁ is empty ; :: thesis: verum