take E = {} (bool the carrier of K); :: thesis: ( E is empty & E is simplex-like )
thus ( E is empty & E is simplex-like ) ; :: thesis: verum