let L be non empty Lattice-like Boolean distributive' LattStr ; :: thesis: Top L = Top' L
set Y = Top L;
( L is upper-bounded' & ( for a being Element of L holds
( (Top L) "/\" a = a & a "/\" (Top L) = a ) ) ) by Th13;
hence Top L = Top' L by Def2; :: thesis: verum