theorem :: ABSRED_0:1

for X being ARS
for a, b being Element of X st a ==> b holds
not X is empty ;