let L be upper-bounded Lattice; :: thesis: Top L = Top (LattPOSet L)
set x = % (Top (LattPOSet L));
now :: thesis: for a being Element of L holds
( (% (Top (LattPOSet L))) "\/" a = % (Top (LattPOSet L)) & a "\/" (% (Top (LattPOSet L))) = % (Top (LattPOSet L)) )
let a be Element of L; :: thesis: ( (% (Top (LattPOSet L))) "\/" a = % (Top (LattPOSet L)) & a "\/" (% (Top (LattPOSet L))) = % (Top (LattPOSet L)) )
a % <= (% (Top (LattPOSet L))) % by YELLOW_0:45;
then a [= % (Top (LattPOSet L)) by LATTICE3:7;
hence ( (% (Top (LattPOSet L))) "\/" a = % (Top (LattPOSet L)) & a "\/" (% (Top (LattPOSet L))) = % (Top (LattPOSet L)) ) by LATTICES:def 3; :: thesis: verum
end;
hence Top L = Top (LattPOSet L) by LATTICES:def 17; :: thesis: verum