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