theorem Th4: :: ABSRED_0:4

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 ) )