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