let B be B_Lattice; :: thesis: for IB, JB being Ideal of B holds (.(IB \/ JB).> = IB "\/" JB
let IB, JB be Ideal of B; :: thesis: (.(IB \/ JB).> = IB "\/" JB
reconsider FB = IB .: , GB = JB .: as Filter of (B .:) ;
thus (.(IB \/ JB).> = <.((IB \/ JB) .:).) by Th36
.= FB "/\" GB by FILTER_0:39
.= IB "\/" JB by Th44 ; :: thesis: verum