let L be Lattice; :: thesis: for p, q, r being Element of L holds
( p is_less_than {q,r} iff p [= q "/\" r )
let p, q, r be Element of L; :: thesis: ( p is_less_than {q,r} iff p [= q "/\" r )
A1: ( q in {q,r} & r in {q,r} ) by TARSKI:def 2;
thus ( p is_less_than {q,r} implies p [= q "/\" r ) :: thesis: ( p [= q "/\" r implies p is_less_than {q,r} )

proof

assume p is_less_than {q,r} ; :: thesis: p [= q "/\" r
then ( p [= q & p [= r ) by A1, Def16;
hence p [= q "/\" r by FILTER_0:7; :: thesis: verum

end;

assume A2: p [= q "/\" r ; :: thesis: p is_less_than {q,r}
let a be Element of L; :: according to LATTICE3:def 16 :: thesis: ( a in {q,r} implies p [= a )
assume a in {q,r} ; :: thesis: p [= a
then ( ( a = q or a = r ) & q "/\" r [= q & r "/\" q [= r & q "/\" r = r "/\" q ) by LATTICES:23, TARSKI:def 2;
hence p [= a by A2, LATTICES:25; :: thesis: verum