let L be Lattice; :: thesis: for p, q being Element of L holds
( p in <.p.) & p "\/" q in <.p.) & q "\/" p in <.p.) )
let p, q be Element of L; :: thesis: ( p in <.p.) & p "\/" q in <.p.) & q "\/" p in <.p.) )
p [= p "\/" q by LATTICES:5;
hence ( p in <.p.) & p "\/" q in <.p.) & q "\/" p in <.p.) ) ; :: thesis: verum