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