set X = the non empty trivial strict TopSpace;

take the non empty trivial strict TopSpace ; :: thesis: ( the non empty trivial strict TopSpace is strict & the non empty trivial strict TopSpace is T_0 & not the non empty trivial strict TopSpace is empty )

thus ( the non empty trivial strict TopSpace is strict & the non empty trivial strict TopSpace is T_0 & not the non empty trivial strict TopSpace is empty ) ; :: thesis: verum

take the non empty trivial strict TopSpace ; :: thesis: ( the non empty trivial strict TopSpace is strict & the non empty trivial strict TopSpace is T_0 & not the non empty trivial strict TopSpace is empty )

thus ( the non empty trivial strict TopSpace is strict & the non empty trivial strict TopSpace is T_0 & not the non empty trivial strict TopSpace is empty ) ; :: thesis: verum