theorem :: XREAL_1:211

for a being Real st 1 <= a holds
a " <= 1