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