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