let x, y be Element of F₁(); :: according to ABSRED_0:def 26 :: thesis: ( x <=*=> y implies x >><< y )
assume x <=*=> y ; :: thesis: x >><< y
then A3: F₂(x) = F₂(y) by A2;
take z = F₂(x); :: according to ABSRED_0:def 21 :: thesis: ( x =*=> z & z <=*= y )
thus ( x =*=> z & z <=*= y ) by A3, A1; :: thesis: verum