theorem :: FILTER_2:51
for L being Lattice
for I, J being Ideal of L holds (.(I \/ J).> = (.(I "\/" J).>