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

proof

assume A3: p is_greater_than {q,r} ; :: thesis: q "\/" r [= p
then A4: q [= p by A1;
r [= p by A2, A3;
hence q "\/" r [= p by A4, FILTER_0:6; :: thesis: verum

end;

assume A5: q "\/" r [= p ; :: thesis: p is_greater_than {q,r}
let a be Element of L; :: according to LATTICE3:def 17 :: thesis: ( a in {q,r} implies a [= p )
assume a in {q,r} ; :: thesis: a [= p
then A6: ( a = q or a = r ) by TARSKI:def 2;
A7: q [= q "\/" r by LATTICES:5;
r [= r "\/" q by LATTICES:5;
hence a [= p by A5, A6, A7, LATTICES:7; :: thesis: verum