let L be non trivial bounded Lattice; :: thesis: Top L <> Bottom L
set p = Top L;
assume A0: Top L = Bottom L ; :: thesis: contradiction
consider p being Element of L such that
A2: p <> Top L by SUBSET_1:50;
Bottom L [= p ;
hence contradiction by A2, A0; :: thesis: verum