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 Th44;
hence ( I c= I "\/" J & J c= I "\/" J ) by FILTER_0:36; :: thesis: verum