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} by TARSKI:def 2;

A2: 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} )

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 A6: ( a = q or a = r ) by TARSKI:def 2;

A7: q "/\" r [= q by LATTICES:6;

r "/\" q [= r by LATTICES:6;

hence p [= a by A5, A6, A7, LATTICES:7; :: thesis: verum

( 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} by TARSKI:def 2;

A2: 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 A5:
p [= q "/\" r
; :: thesis: p is_less_than {q,r}
assume A3:
p is_less_than {q,r}
; :: thesis: p [= q "/\" r

then A4: p [= q by A1;

p [= r by A2, A3;

hence p [= q "/\" r by A4, FILTER_0:7; :: thesis: verum

end;then A4: p [= q by A1;

p [= r by A2, A3;

hence p [= q "/\" r by A4, FILTER_0:7; :: thesis: verum

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 A6: ( a = q or a = r ) by TARSKI:def 2;

A7: q "/\" r [= q by LATTICES:6;

r "/\" q [= r by LATTICES:6;

hence p [= a by A5, A6, A7, LATTICES:7; :: thesis: verum