let X be ARS ; :: thesis: ( X is WN & X is UN implies X is CR )
assume A1: X is WN ; :: thesis: ( not X is UN or X is CR )
assume A2: X is UN ; :: thesis: X is CR
let x be Element of X; :: according to ABSRED_0:def 26 :: thesis: for y being Element of X st x <=*=> y holds
x >><< y
let y be Element of X; :: thesis: ( x <=*=> y implies x >><< y )
assume A3: x <=*=> y ; :: thesis: x >><< y
A4: ( x is normalizable & y is normalizable ) by A1;
consider u being Element of X such that
A5: u is_normform_of x by A4;
consider v being Element of X such that
A6: v is_normform_of y by A4;
A7: ( u is normform & x =*=> u ) by A5;
take u ; :: according to ABSRED_0:def 21 :: thesis: ( x =*=> u & u <=*= y )
thus x =*=> u by A5; :: thesis: u <=*= y
u <=*=> x by A5, LemZ;
then ( u <=*=> y & y <=*=> v ) by A3, A6, Th7, LemZ;
hence y =*=> u by A2, A7, A6, Th7; :: thesis: verum