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 )
A2: (f,O1) +. a [= (f,(succ O1)) +. a by A1, Th24, 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,(succ O1)) +. a [= (f,O2) +. a by A1, Th24;
then (f,O1) +. a = (f,(succ O1)) +. a by A5, A2, LATTICES:8;
then (f,O1) +. a = f . ((f,O1) +. a) by Th15;
hence contradiction by A4, A5; :: thesis: verum