let L be non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' LattStr ; :: thesis: Top L = Top' L
A1: L is upper-bounded by Th13;
set Y = Top' L;
for a being Element of L holds
( (Top' L) "\/" a = Top' L & a "\/" (Top' L) = Top' L ) by Th5;
hence Top L = Top' L by A1, LATTICES:def 17; :: thesis: verum