A1: r in REAL by XREAL_0:def 1;
A c= REAL by MEMBERED:3;
hence r ** A is bounded_above by A1, INTEGRA2:12; :: thesis: verum