:: deftheorem defines WCR ABSRED_0:def 27 :
for X being ARS holds
( X is WCR iff for x, y being Element of X st x <<01>> y holds
x >><< y );