let X be ARS ; :: thesis: ( X is CR implies X is N.F. )

assume A1: X is CR ; :: thesis: X is N.F.

let x be Element of X; :: according to ABSRED_0:def 18 :: thesis: for y being Element of X st x is normform & x <=*=> y holds

y =*=> x

let y be Element of X; :: thesis: ( x is normform & x <=*=> y implies y =*=> x )

assume A2: x is normform ; :: thesis: ( not x <=*=> y or y =*=> x )

assume A3: x <=*=> y ; :: thesis: y =*=> x

A4: x >><< y by A1, A3;

consider z being Element of X such that

A5: ( x =*=> z & z <=*= y ) by A4;

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

assume A1: X is CR ; :: thesis: X is N.F.

let x be Element of X; :: according to ABSRED_0:def 18 :: thesis: for y being Element of X st x is normform & x <=*=> y holds

y =*=> x

let y be Element of X; :: thesis: ( x is normform & x <=*=> y implies y =*=> x )

assume A2: x is normform ; :: thesis: ( not x <=*=> y or y =*=> x )

assume A3: x <=*=> y ; :: thesis: y =*=> x

A4: x >><< y by A1, A3;

consider z being Element of X such that

A5: ( x =*=> z & z <=*= y ) by A4;

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