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