let X be set ; :: thesis: for L being Lattice
for p9 being Element of (LattPOSet L) holds
( X is_<=_than p9 iff X is_less_than % p9 )
let L be Lattice; :: thesis: for p9 being Element of (LattPOSet L) holds
( X is_<=_than p9 iff X is_less_than % p9 )
let p9 be Element of (LattPOSet L); :: thesis: ( X is_<=_than p9 iff X is_less_than % p9 )
(% p9) % = % p9 ;
hence ( X is_<=_than p9 iff X is_less_than % p9 ) by Th30; :: thesis: verum