{} K is simplex-like ;
hence ex b₁ being Simplex of K st b₁ is empty ; :: thesis: verum