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