let X be ARS ; :: thesis: for x, y being Element of X st X is WN & X is UN* & x is normform & x <=*=> y holds
y =*=> x
let x, y be Element of X; :: thesis: ( X is WN & X is UN* & x is normform & x <=*=> y implies y =*=> x )
assume A1: ( X is WN & X is UN* ) ; :: thesis: ( not x is normform or not x <=*=> y or y =*=> x )
assume A2: x is normform ; :: thesis: ( not x <=*=> y or y =*=> x )
assume A3: x <=*=> y ; :: thesis: y =*=> x
defpred S₁[ Element of X] means $1 =*=> x;
A4: 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 B1: y <==> z ; :: thesis: ( not S₁[y] or S₁[z] )
assume B2: S₁[y] ; :: thesis: S₁[z]

per cases ( y ==> z or y <== z ) by B1;

suppose C1: y ==> z ; :: thesis: S₁[z]

B3: z is normalizable by A1;
consider u being Element of X such that
B4: u is_normform_of z by B3;
B5: u is_normform_of y by C1, B4, LemN6;
B6: x is_normform_of y by A2, B2;
thus S₁[z] by B4, B6, B5, A1; :: thesis: verum

end;

suppose C2: y <== z ; :: thesis: S₁[z]

thus S₁[z] by B2, C2, Lem5; :: thesis: verum

end;

end;

end;

A5: for y, z being Element of X st y <=*=> z & S₁[y] holds
S₁[z] from ABSRED_0:sch 5(A4);
thus y =*=> x by A3, A5; :: thesis: verum