theorem Th8: :: ABSRED_0:8

for X being ARS
for x, y being Element of X holds
( x <=+=> y iff ex z being Element of X st
( x <=*=> z & z <==> y ) )