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 )
succ O1 = O1 \/ {O1} by ORDINAL1:def 1;
then A2: f,O1 +. a [= f,(succ O1) +. a by A1, Th27, XBOOLE_1:7;
assume that
A3: O1 c< O2 and
A4: not f,O2 +. a is_a_fixpoint_of f and
A5: f,O1 +. a = f,O2 +. a ; :: thesis: contradiction
O1 in O2 by A3, ORDINAL1:21;
then succ O1 c= O2 by ORDINAL1:33;
then f,(succ O1) +. a [= f,O2 +. a by A1, Th27;
then f,O1 +. a = f,(succ O1) +. a by A5, A2, LATTICES:26;
then f,O1 +. a = f . (f,O1 +. a) by Th18;
hence contradiction by A4, A5, ABIAN:def 4; :: thesis: verum