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_{1} being Element of the carrier of E holds a = b_{1}

take b ; :: thesis: not a = b

thus not a = b ; :: thesis: verum

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

take b ; :: thesis: not a = b

thus not a = b ; :: thesis: verum