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