:: deftheorem defines <= OSALG_1:def 6 :
for S being non empty Poset
for w1, w2 being Element of the carrier of S * holds
( w1 <= w2 iff ( len w1 = len w2 & ( for i being set st i in dom w1 holds
for s1, s2 being Element of S st s1 = w1 . i & s2 = w2 . i holds
s1 <= s2 ) ) );