let L be Lattice; :: thesis: for I, J being Ideal of L holds
( I c= I "\/" J & J c= I "\/" J )
let I, J be Ideal of L; :: thesis: ( I c= I "\/" J & J c= I "\/" J )
I "\/" J = (I .: ) "/\" (J .: ) by Th45;
hence ( I c= I "\/" J & J c= I "\/" J ) by FILTER_0:49; :: thesis: verum