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₁[ 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₁[y] holds
S₁[z]

proof

let y, z be Element of X; :: thesis: ( y <==> z & S₁[y] implies S₁[z] )
assume A3: y <==> z ; :: thesis: ( not S₁[y] or S₁[z] )
given u being Element of X such that A4: ( x <=*=> u & u <==> y ) ; :: thesis: S₁[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;

A5: for y, z being Element of X st y <=*=> z & S₁[y] holds
S₁[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