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