for A being non empty RelStr
for a1, a2 being Element of A holds
( not A is strongly_connected or a1 = a2 or a1 < a2 or a2 < a1 )