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