:: deftheorem defines < SRINGS_5:def 19 :
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 );