let X be ARS ; :: thesis: for x, y being Element of X st x <> y & ( for a, b being Element of X holds

( a ==> b iff a = x ) ) holds

( y is normform & x is normalizable )

let x, y be Element of X; :: thesis: ( x <> y & ( for a, b being Element of X holds

( a ==> b iff a = x ) ) implies ( y is normform & x is normalizable ) )

assume Z0: x <> y ; :: thesis: ( ex a, b being Element of X st

( ( a ==> b implies a = x ) implies ( a = x & not a ==> b ) ) or ( y is normform & x is normalizable ) )

assume Z2: for a, b being Element of X holds

( a ==> b iff a = x ) ; :: thesis: ( y is normform & x is normalizable )

thus y is normform by Z0, Z2; :: thesis: x is normalizable

take y ; :: according to ABSRED_0:def 13 :: thesis: y is_normform_of x

thus y is normform by Z0, Z2; :: according to ABSRED_0:def 12 :: thesis: x =*=> y

thus x =*=> y by Z2, Th2; :: thesis: verum

( a ==> b iff a = x ) ) holds

( y is normform & x is normalizable )

let x, y be Element of X; :: thesis: ( x <> y & ( for a, b being Element of X holds

( a ==> b iff a = x ) ) implies ( y is normform & x is normalizable ) )

assume Z0: x <> y ; :: thesis: ( ex a, b being Element of X st

( ( a ==> b implies a = x ) implies ( a = x & not a ==> b ) ) or ( y is normform & x is normalizable ) )

assume Z2: for a, b being Element of X holds

( a ==> b iff a = x ) ; :: thesis: ( y is normform & x is normalizable )

thus y is normform by Z0, Z2; :: thesis: x is normalizable

take y ; :: according to ABSRED_0:def 13 :: thesis: y is_normform_of x

thus y is normform by Z0, Z2; :: according to ABSRED_0:def 12 :: thesis: x =*=> y

thus x =*=> y by Z2, Th2; :: thesis: verum