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

proof

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

end;

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