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 )
A2: (f,(succ O1)) -. a [= (f,O1) -. a by A1, Th25, 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:11;
then succ O1 c= O2 by ORDINAL1:21;
then (f,O2) -. a [= (f,(succ O1)) -. a by A1, Th25;
then (f,O1) -. a = (f,(succ O1)) -. a by A5, A2, LATTICES:8;
then (f,O1) -. a = f . ((f,O1) -. a) by Th16;
hence contradiction by A4, A5; :: thesis: verum