let A be non empty set ; :: thesis: RealFunc_Lattice A is D_Lattice
for p, q, r being Element of (RealFunc_Lattice A) holds p "/\" (q "\/" r) = (p "/\" q) "\/" (p "/\" r) by Th20;
hence RealFunc_Lattice A is D_Lattice by LATTICES:def 11; :: thesis: verum