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 p9 be Element of (LattPOSet L); :: according to LATTICE3:def 8 :: thesis: ( p9 in X implies p % <= p9 )
A2: (% p9) % = % p9 ;
assume p9 in X ; :: thesis: p % <= p9
then p [= % p9 by A1;
hence p % <= p9 by A2, Th7; :: thesis: verum

end;

assume A3: for q9 being Element of (LattPOSet L) st q9 in X holds
p % <= q9 ; :: 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