let r, s be Real; :: thesis: ( [r,s] in RealOrd implies r <= s )

hereby :: thesis: verum

assume [r,s] in RealOrd ; :: thesis: r <= s
then consider r1, s1 being Real such that
A1: [r,s] = [r1,s1] and
A2: r1 <= s1 ;
r = r1 by A1, XTUPLE_0:1;
hence r <= s by A1, A2, XTUPLE_0:1; :: thesis: verum

end;