let L be complete Lattice; 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; 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; ( 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
; 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; ( 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
; 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; verum