let X be set ; :: thesis: for L being Lattice
for p being Element of L holds
( p is_less_than X iff p % is_<=_than X )
let L be Lattice; :: thesis: for p being Element of L holds
( p is_less_than X iff p % is_<=_than X )
let p be Element of L; :: thesis: ( p is_less_than X iff p % is_<=_than X )
thus ( p is_less_than X implies p % is_<=_than X ) :: thesis: ( p % is_<=_than X implies p is_less_than X )

proof

assume A1: for q being Element of L st q in X holds
p [= q ; :: according to LATTICE3:def 16 :: thesis: p % is_<=_than X
let p' be Element of (LattPOSet L); :: according to LATTICE3:def 8 :: thesis: ( p' in X implies p % <= p' )
A2: ( p' = % p' & (% p') % = % p' ) ;
assume p' in X ; :: thesis: p % <= p'
then p [= % p' by A1;
hence p % <= p' by A2, Th7; :: thesis: verum

end;

assume A3: for q' being Element of (LattPOSet L) st q' in X holds
p % <= q' ; :: according to LATTICE3:def 8 :: thesis: p is_less_than X
let q be Element of L; :: according to LATTICE3:def 16 :: thesis: ( q in X implies p [= q )
assume q in X ; :: thesis: p [= q
then p % <= q % by A3;
hence p [= q by Th7; :: thesis: verum