theorem :: REAL_LAT:28

for A being non empty set holds RealFunc_Lattice A is D_Lattice