take E = {} (bool the carrier of K); :: thesis: ( E is empty & E is simplex-like )
for A being Subset of K st A in E holds
A is simplex-like ;
hence ( E is empty & E is simplex-like ) by TOPS_2:def 1; :: thesis: verum