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).>
A1: (.(I "\/" J).> = <.((I "\/" J) .: ).) by Th37;
( (.(I \/ J).> = <.((I \/ J) .: ).) & (I .: ) "/\" (J .: ) = I "\/" J ) by Th37, Th45;
hence (.(I \/ J).> = (.(I "\/" J).> by A1, FILTER_0:50; :: thesis: verum