consider T being non empty TopSpace;
reconsider E = OpenClosedSetLatt T as B_Lattice by Th14;
reconsider a = [#] T, b = {} T as Element of E by Th7, Th8;
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