:: deftheorem Def5 defines <=E DICKSON:def 5 :
for R being RelStr
for b₂ being Relation of (Class (EqRel R)) holds
( b₂ = <=E R iff for A, B being object holds
( [A,B] in b₂ iff ex a, b being Element of R st
( A = Class ((EqRel R),a) & B = Class ((EqRel R),b) & a <= b ) ) );