let x, y be Element of F_{1}(); :: according to ABSRED_0:def 26 :: thesis: ( x <=*=> y implies x >><< y )

assume x <=*=> y ; :: thesis: x >><< y

then A3: F_{2}(x) = F_{2}(y)
by A2;

take z = F_{2}(x); :: according to ABSRED_0:def 21 :: thesis: ( x =*=> z & z <=*= y )

thus ( x =*=> z & z <=*= y ) by A3, A1; :: thesis: verum

assume x <=*=> y ; :: thesis: x >><< y

then A3: F

take z = F

thus ( x =*=> z & z <=*= y ) by A3, A1; :: thesis: verum