set T = the non empty trivial strict TopSpace;
take the non empty trivial strict TopSpace ; :: thesis: ( the non empty trivial strict TopSpace is strict & not the non empty trivial strict TopSpace is empty & the non empty trivial strict TopSpace is trivial )
thus ( the non empty trivial strict TopSpace is strict & not the non empty trivial strict TopSpace is empty & the non empty trivial strict TopSpace is trivial ) ; :: thesis: verum