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_{1}[ Element of X] means $1 =*=> x;

A4: 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(A4);

thus y =*=> x by A3, A5; :: thesis: verum

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

A4: 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 B1: y <==> z ; :: thesis: ( not S_{1}[y] or S_{1}[z] )

assume B2: S_{1}[y]
; :: thesis: S_{1}[z]

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

assume B2: S

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

end;

suppose C1:
y ==> z
; :: thesis: S_{1}[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_{1}[z]
by B4, B6, B5, A1; :: thesis: verum

end;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

S

thus y =*=> x by A3, A5; :: thesis: verum