for A being non empty set holds RealFunc_Lattice A is D_Lattice