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