set T = the non empty TopSpace;
reconsider E = OpenClosedSetLatt the non empty TopSpace as B_Lattice ;
reconsider a = [#] the non empty TopSpace, b = {} the non empty TopSpace as Element of E by Th3;
take E ; :: thesis: not E is trivial
take a ; :: according to STRUCT_0:def 10 :: thesis: not for b₁ being Element of the carrier of E holds a = b₁
take b ; :: thesis: not a = b
thus not a = b ; :: thesis: verum