A1: ( 0 in REAL & 1 in REAL ) by XREAL_0:def 1;
thus ex a, b being Element of G_Real st a <> b by A1; :: thesis: verum