theorem :: WAYBEL_3:14

for L being non empty reflexive antisymmetric RelStr
for x, y being Element of L st not x is compact & x << y holds
x < y by Th1;