set T = the non empty TopSpace;
set OL = Open_setLatt the non empty TopSpace;
the carrier of the non empty TopSpace = Top (Open_setLatt the non empty TopSpace) by Th9;
then reconsider a = the carrier of the non empty TopSpace as Element of (Open_setLatt the non empty TopSpace) ;
{} = Bottom (Open_setLatt the non empty TopSpace) by Th8;
then reconsider b = {} as Element of (Open_setLatt the non empty TopSpace) ;
take Open_setLatt the non empty TopSpace ; :: thesis: not Open_setLatt the non empty TopSpace is trivial
take a ; :: according to STRUCT_0:def 10 :: thesis: not for b₁ being Element of the carrier of (Open_setLatt the non empty TopSpace) holds a = b₁
take b ; :: thesis: not a = b
thus not a = b ; :: thesis: verum