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