let X be ARS ; :: thesis: for x being Element of X holds

( x is normform iff x is_a_normal_form_wrt the reduction of X )

let x be Element of X; :: thesis: ( x is normform iff x is_a_normal_form_wrt the reduction of X )

set R = the reduction of X;

thus ( x is normform implies x is_a_normal_form_wrt the reduction of X ) :: thesis: ( x is_a_normal_form_wrt the reduction of X implies x is normform )

let y be Element of X; :: according to ABSRED_0:def 11 :: thesis: not x ==> y

assume [x,y] in the reduction of X ; :: according to ABSRED_0:def 1 :: thesis: contradiction

hence contradiction by Z1; :: thesis: verum

( x is normform iff x is_a_normal_form_wrt the reduction of X )

let x be Element of X; :: thesis: ( x is normform iff x is_a_normal_form_wrt the reduction of X )

set R = the reduction of X;

thus ( x is normform implies x is_a_normal_form_wrt the reduction of X ) :: thesis: ( x is_a_normal_form_wrt the reduction of X implies x is normform )

proof

assume Z1:
for b being object holds not [x,b] in the reduction of X
; :: according to REWRITE1:def 5 :: thesis: x is normform
assume Z0:
for y being Element of X holds not x ==> y
; :: according to ABSRED_0:def 11 :: thesis: x is_a_normal_form_wrt the reduction of X

let a be object ; :: according to REWRITE1:def 5 :: thesis: not [x,a] in the reduction of X

assume Z1: [x,a] in the reduction of X ; :: thesis: contradiction

then reconsider y = a as Element of X by ZFMISC_1:87;

x ==> y by Z1;

hence contradiction by Z0; :: thesis: verum

end;let a be object ; :: according to REWRITE1:def 5 :: thesis: not [x,a] in the reduction of X

assume Z1: [x,a] in the reduction of X ; :: thesis: contradiction

then reconsider y = a as Element of X by ZFMISC_1:87;

x ==> y by Z1;

hence contradiction by Z0; :: thesis: verum

let y be Element of X; :: according to ABSRED_0:def 11 :: thesis: not x ==> y

assume [x,y] in the reduction of X ; :: according to ABSRED_0:def 1 :: thesis: contradiction

hence contradiction by Z1; :: thesis: verum