let x, y be Element of X; :: thesis: ( ex z being Element of X st

( x <==> z & z <=*=> y ) implies ex z being Element of X st

( y <==> z & z <=*=> x ) )

given z being Element of X such that A1: ( x <==> z & z <=*=> y ) ; :: thesis: ex z being Element of X st

( y <==> z & z <=*=> x )

defpred S_{1}[ Element of X] means ex u being Element of X st

( x <=*=> u & u <==> $1 );

A2: for y, z being Element of X st y <==> z & S_{1}[y] holds

S_{1}[z]
_{1}[y] holds

S_{1}[z]
from ABSRED_0:sch 5(A2);

ex u being Element of X st

( x <=*=> u & u <==> y ) by A1, A5;

hence ex z being Element of X st

( y <==> z & z <=*=> x ) ; :: thesis: verum

( x <==> z & z <=*=> y ) implies ex z being Element of X st

( y <==> z & z <=*=> x ) )

given z being Element of X such that A1: ( x <==> z & z <=*=> y ) ; :: thesis: ex z being Element of X st

( y <==> z & z <=*=> x )

defpred S

( x <=*=> u & u <==> $1 );

A2: for y, z being Element of X st y <==> z & S

S

proof

A5:
for y, z being Element of X st y <=*=> z & S
let y, z be Element of X; :: thesis: ( y <==> z & S_{1}[y] implies S_{1}[z] )

assume A3: y <==> z ; :: thesis: ( not S_{1}[y] or S_{1}[z] )

given u being Element of X such that A4: ( x <=*=> u & u <==> y ) ; :: thesis: S_{1}[z]

take y ; :: thesis: ( x <=*=> y & y <==> z )

u <=*=> y by A4, Th6;

hence ( x <=*=> y & y <==> z ) by A3, A4, Th7; :: thesis: verum

end;assume A3: y <==> z ; :: thesis: ( not S

given u being Element of X such that A4: ( x <=*=> u & u <==> y ) ; :: thesis: S

take y ; :: thesis: ( x <=*=> y & y <==> z )

u <=*=> y by A4, Th6;

hence ( x <=*=> y & y <==> z ) by A3, A4, Th7; :: thesis: verum

S

ex u being Element of X st

( x <=*=> u & u <==> y ) by A1, A5;

hence ex z being Element of X st

( y <==> z & z <=*=> x ) ; :: thesis: verum