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 & p "\/" q = q "\/" p ) by LATTICES:22;
hence ( p in <.p.) & p "\/" q in <.p.) & q "\/" p in <.p.) ) ; :: thesis: verum