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

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