let L be Lattice; :: thesis: for p, r, q being Element of L st p [= r holds
p [= q "\/" r
let p, r, q be Element of L; :: thesis: ( p [= r implies p [= q "\/" r )
assume p [= r ; :: thesis: p [= q "\/" r
then ( p "\/" q [= r "\/" q & q "\/" p [= q "\/" r & p [= p "\/" q & q "\/" p = p "\/" q ) by Th1, LATTICES:22;
hence p [= q "\/" r by LATTICES:25; :: thesis: verum