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