let L be complete Lattice; :: thesis: for f being monotone UnOp of L
for a being Element of L st a [= f . a holds
for O1, O2 being Ordinal st O1 c< O2 & not f,O2 +. a is_a_fixpoint_of f holds
f,O1 +. a <> f,O2 +. a
let f be monotone UnOp of L; :: thesis: for a being Element of L st a [= f . a holds
for O1, O2 being Ordinal st O1 c< O2 & not f,O2 +. a is_a_fixpoint_of f holds
f,O1 +. a <> f,O2 +. a
let a be Element of L; :: thesis: ( a [= f . a implies for O1, O2 being Ordinal st O1 c< O2 & not f,O2 +. a is_a_fixpoint_of f holds
f,O1 +. a <> f,O2 +. a )
assume A1: a [= f . a ; :: thesis: for O1, O2 being Ordinal st O1 c< O2 & not f,O2 +. a is_a_fixpoint_of f holds
f,O1 +. a <> f,O2 +. a
let O1, O2 be Ordinal; :: thesis: ( O1 c< O2 & not f,O2 +. a is_a_fixpoint_of f implies f,O1 +. a <> f,O2 +. a )
assume A2: ( O1 c< O2 & not f,O2 +. a is_a_fixpoint_of f & f,O1 +. a = f,O2 +. a ) ; :: thesis: contradiction
then O1 in O2 by ORDINAL1:21;
then succ O1 c= O2 by ORDINAL1:33;
then A3: f,(succ O1) +. a [= f,O2 +. a by A1, Th27;
succ O1 = O1 \/ {O1} by ORDINAL1:def 1;
then f,O1 +. a [= f,(succ O1) +. a by A1, Th27, XBOOLE_1:7;
then f,O1 +. a = f,(succ O1) +. a by A2, A3, LATTICES:26;
then f,O1 +. a = f . (f,O1 +. a) by Th18;
hence contradiction by A2, ABIAN:def 4; :: thesis: verum