:: deftheorem defines <= SRINGS_5:def 18 :
for n being Nat
for a, b being Element of REAL n holds
( a <= b iff for i being Nat st i in Seg n holds
a . i <= b . i );