field RealOrd c= REAL \/ REAL by RELSET_1:8;
hence field RealOrd c= REAL ; :: according to XBOOLE_0:def 10 :: thesis: REAL c= field RealOrd
thus REAL c= field RealOrd by Lm1, PARTIT_2:8; :: thesis: verum