let L be complete Lattice; :: thesis: for f being monotone UnOp of L
for a being Element of L st f . a [= 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 f . a [= 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: ( f . a [= 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: f . a [= 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,(succ O1) -. a [= f,O1 -. a by A1, Th28, 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,O2 -. a [= f,(succ O1) -. a by A1, Th28;
then f,O1 -. a = f,(succ O1) -. a by A5, A2, LATTICES:26;
then f,O1 -. a = f . (f,O1 -. a) by Th19;
hence contradiction by A4, A5, ABIAN:def 4; :: thesis: verum