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