knaster.miz



    begin

    reserve f,g,h for Function;

    theorem :: KNASTER:1

    h = (f \/ g) & ( dom f) misses ( dom g) implies (h is one-to-one iff f is one-to-one & g is one-to-one & ( rng f) misses ( rng g))

    proof

      assume that

       A1: h = (f \/ g) and

       A2: ( dom f) misses ( dom g);

      

       A3: ( dom h) = (( dom f) \/ ( dom g)) by A1, XTUPLE_0: 23;

      hereby

        assume

         A4: h is one-to-one;

        thus f is one-to-one

        proof

          assume not f is one-to-one;

          then

          consider x1,x2 be object such that

           A5: x1 in ( dom f) and

           A6: x2 in ( dom f) and

           A7: (f . x1) = (f . x2) & x1 <> x2;

          

           A8: x2 in ( dom h) by A3, A6, XBOOLE_0:def 3;

           [x2, (f . x2)] in f by A6, FUNCT_1:def 2;

          then [x2, (f . x2)] in h by A1, XBOOLE_0:def 3;

          then

           A9: (f . x2) = (h . x2) by A8, FUNCT_1:def 2;

          

           A10: x1 in ( dom h) by A3, A5, XBOOLE_0:def 3;

           [x1, (f . x1)] in f by A5, FUNCT_1:def 2;

          then [x1, (f . x1)] in h by A1, XBOOLE_0:def 3;

          then (f . x1) = (h . x1) by A10, FUNCT_1:def 2;

          hence contradiction by A4, A7, A10, A8, A9;

        end;

        thus g is one-to-one

        proof

          assume not g is one-to-one;

          then

          consider x1,x2 be object such that

           A11: x1 in ( dom g) and

           A12: x2 in ( dom g) and

           A13: (g . x1) = (g . x2) & x1 <> x2;

          

           A14: x2 in ( dom h) by A3, A12, XBOOLE_0:def 3;

           [x2, (g . x2)] in g by A12, FUNCT_1:def 2;

          then [x2, (g . x2)] in h by A1, XBOOLE_0:def 3;

          then

           A15: (g . x2) = (h . x2) by A14, FUNCT_1:def 2;

          

           A16: x1 in ( dom h) by A3, A11, XBOOLE_0:def 3;

           [x1, (g . x1)] in g by A11, FUNCT_1:def 2;

          then [x1, (g . x1)] in h by A1, XBOOLE_0:def 3;

          then (g . x1) = (h . x1) by A16, FUNCT_1:def 2;

          hence contradiction by A4, A13, A16, A14, A15;

        end;

        thus ( rng f) misses ( rng g)

        proof

          assume not thesis;

          then

          consider hx be object such that

           A17: hx in ( rng f) and

           A18: hx in ( rng g) by XBOOLE_0: 3;

          consider x1 be object such that

           A19: x1 in ( dom f) and

           A20: hx = (f . x1) by A17, FUNCT_1:def 3;

          

           A21: x1 in ( dom h) by A3, A19, XBOOLE_0:def 3;

          consider x2 be object such that

           A22: x2 in ( dom g) and

           A23: hx = (g . x2) by A18, FUNCT_1:def 3;

          

           A24: x2 in ( dom h) by A3, A22, XBOOLE_0:def 3;

          

           A25: hx is set by TARSKI: 1;

           [x2, hx] in g by A22, A23, FUNCT_1:def 2;

          then [x2, hx] in h by A1, XBOOLE_0:def 3;

          then

           A26: (h . x2) = hx by A24, FUNCT_1:def 2, A25;

          

           A27: x1 <> x2 by A2, A19, A22, XBOOLE_0: 3;

           [x1, hx] in f by A19, A20, FUNCT_1:def 2;

          then [x1, hx] in h by A1, XBOOLE_0:def 3;

          then (h . x1) = hx by A21, FUNCT_1:def 2, A25;

          hence contradiction by A4, A27, A21, A24, A26;

        end;

      end;

      assume

       A28: f is one-to-one & g is one-to-one & ( rng f) misses ( rng g);

      (f \/ g) = (f +* g) by A2, FUNCT_4: 31;

      hence thesis by A1, A28, FUNCT_4: 92;

    end;

    begin

    reserve x,y,z,u,X for set,

A for non empty set,

n for Element of NAT ,

f for Function of X, X;

    theorem :: KNASTER:2

    

     Th2: x is_a_fixpoint_of ( iter (f,n)) implies (f . x) is_a_fixpoint_of ( iter (f,n))

    proof

      assume

       A1: x is_a_fixpoint_of ( iter (f,n));

      then

       A2: x in ( dom ( iter (f,n)));

      

       A3: ( dom f) = X by FUNCT_2: 52;

      then ( dom ( iter (f,n))) = X & (f . x) in ( rng f) by A2, FUNCT_1:def 3, FUNCT_2: 52;

      hence (f . x) in ( dom ( iter (f,n)));

      x = (( iter (f,n)) . x) by A1;

      

      hence (f . x) = ((f * ( iter (f,n))) . x) by A2, FUNCT_1: 13

      .= (( iter (f,(n + 1))) . x) by FUNCT_7: 71

      .= ((( iter (f,n)) * f) . x) by FUNCT_7: 69

      .= (( iter (f,n)) . (f . x)) by A2, A3, FUNCT_1: 13;

    end;

    theorem :: KNASTER:3

    (ex n st x is_a_fixpoint_of ( iter (f,n)) & for y st y is_a_fixpoint_of ( iter (f,n)) holds x = y) implies x is_a_fixpoint_of f

    proof

      given n such that

       A1: x is_a_fixpoint_of ( iter (f,n)) and

       A2: for y st y is_a_fixpoint_of ( iter (f,n)) holds x = y;

      ( dom f) = X & ( dom ( iter (f,n))) = X by FUNCT_2: 52;

      hence x in ( dom f) by A1;

      thus thesis by A1, A2, Th2;

    end;

    definition

      let A,B be non empty set, f be Function of A, B;

      :: original: c=-monotone

      redefine

      :: KNASTER:def1

      attr f is c=-monotone means

      : Def1: for x,y be Element of A st x c= y holds (f . x) c= (f . y);

      compatibility

      proof

        ( dom f) = A by FUNCT_2:def 1;

        hence f is c=-monotone implies for x,y be Element of A st x c= y holds (f . x) c= (f . y);

        assume

         A1: for x,y be Element of A st x c= y holds (f . x) c= (f . y);

        let x,y be set;

        assume x in ( dom f) & y in ( dom f) & x c= y;

        hence thesis by A1;

      end;

    end

    registration

      let A be set, B be non empty set;

      cluster c=-monotone for Function of A, B;

      existence

      proof

        set b = the Element of B;

        reconsider f = (A --> b) as Function of A, B;

        take f;

        let x,y be set;

        assume that

         A1: x in ( dom f) and

         A2: y in ( dom f) and x c= y;

        (f . x) = b by A1, FUNCOP_1: 7

        .= (f . y) by A2, FUNCOP_1: 7;

        hence thesis;

      end;

    end

    definition

      let X be set;

      let f be c=-monotone Function of ( bool X), ( bool X);

      :: KNASTER:def2

      func lfp (X,f) -> Subset of X equals ( meet { h where h be Subset of X : (f . h) c= h });

      coherence

      proof

        defpred P[ set] means (f . $1) c= $1;

        reconsider H = { h where h be Subset of X : P[h] } as Subset-Family of X from DOMAIN_1:sch 7;

        reconsider H as Subset-Family of X;

        ( meet H) is Subset of X;

        hence thesis;

      end;

      :: KNASTER:def3

      func gfp (X,f) -> Subset of X equals ( union { h where h be Subset of X : h c= (f . h) });

      coherence

      proof

        defpred P[ set] means $1 c= (f . $1);

        reconsider H = { h where h be Subset of X : P[h] } as Subset-Family of X from DOMAIN_1:sch 7;

        ( union H) is Subset of X;

        hence thesis;

      end;

    end

    reserve f for c=-monotone Function of ( bool X), ( bool X),

S for Subset of X;

    theorem :: KNASTER:4

    

     Th4: ( lfp (X,f)) is_a_fixpoint_of f

    proof

      defpred P[ set] means (f . $1) c= $1;

      reconsider H = { h where h be Subset of X : P[h] } as Subset-Family of X from DOMAIN_1:sch 7;

      reconsider H as Subset-Family of X;

      set A = ( meet H);

      now

        X c= X;

        then

        reconsider X9 = X as Subset of X;

        (f . X9) c= X9;

        then X9 in H;

        hence H <> {} ;

        let h be set;

        assume

         A1: h in H;

        then

        consider x be Subset of X such that

         A2: x = h and

         A3: (f . x) c= x;

        A c= h by A1, SETFAM_1: 3;

        then (f . A) c= (f . x) by A2, Def1;

        hence (f . A) c= h by A2, A3;

      end;

      then

       A4: (f . A) c= A by SETFAM_1: 5;

      then (f . (f . A)) c= (f . A) by Def1;

      then (f . A) in H;

      then A c= (f . A) by SETFAM_1: 3;

      hence (f . ( lfp (X,f))) = ( lfp (X,f)) by A4;

    end;

    theorem :: KNASTER:5

    

     Th5: ( gfp (X,f)) is_a_fixpoint_of f

    proof

      defpred P[ set] means $1 c= (f . $1);

      reconsider H = { h where h be Subset of X : P[h] } as Subset-Family of X from DOMAIN_1:sch 7;

      set A = ( union H);

      now

        let x be set;

        assume

         A1: x in H;

        then

        consider h be Subset of X such that

         A2: x = h and

         A3: h c= (f . h);

        h c= A by A1, A2, ZFMISC_1: 74;

        then (f . h) c= (f . A) by Def1;

        hence x c= (f . A) by A2, A3;

      end;

      then

       A4: A c= (f . A) by ZFMISC_1: 76;

      then (f . A) c= (f . (f . A)) by Def1;

      then (f . A) in H;

      then (f . A) c= A by ZFMISC_1: 74;

      hence (f . ( gfp (X,f))) = ( gfp (X,f)) by A4;

    end;

    theorem :: KNASTER:6

    

     Th6: (f . S) c= S implies ( lfp (X,f)) c= S

    proof

      set H = { h where h be Subset of X : (f . h) c= h };

      assume (f . S) c= S;

      then S in H;

      hence thesis by SETFAM_1: 3;

    end;

    theorem :: KNASTER:7

    

     Th7: S c= (f . S) implies S c= ( gfp (X,f))

    proof

      set H = { h where h be Subset of X : h c= (f . h) };

      assume S c= (f . S);

      then S in H;

      hence thesis by ZFMISC_1: 74;

    end;

    theorem :: KNASTER:8

    

     Th8: S is_a_fixpoint_of f implies ( lfp (X,f)) c= S & S c= ( gfp (X,f)) by Th6, Th7;

    ::$Notion-Name

    scheme :: KNASTER:sch1

    Knaster { A() -> set , F( object) -> set } :

ex D be set st F(D) = D & D c= A()

      provided

       A1: for X,Y be set st X c= Y holds F(X) c= F(Y)

       and

       A2: F(A) c= A();

      consider f be Function such that

       A3: ( dom f) = ( bool A()) & for x be object st x in ( bool A()) holds (f . x) = F(x) from FUNCT_1:sch 3;

      ( rng f) c= ( bool A())

      proof

        let x be object;

        assume x in ( rng f);

        then

        consider y be object such that

         A4: y in ( dom f) and

         A5: x = (f . y) by FUNCT_1:def 3;

        F(y) c= F(A) by A1, A3, A4;

        then F(y) c= A() by A2;

        then (f . y) c= A() by A3, A4;

        hence thesis by A5;

      end;

      then

      reconsider f as Function of ( bool A()), ( bool A()) by A3, FUNCT_2:def 1, RELSET_1: 4;

      now

        let a,b be set;

        assume that

         A6: a in ( dom f) & b in ( dom f) and

         A7: a c= b;

        (f . a) = F(a) & (f . b) = F(b) by A3, A6;

        hence (f . a) c= (f . b) by A1, A7;

      end;

      then

      reconsider f as c=-monotone Function of ( bool A()), ( bool A()) by COHSP_1:def 11;

      take d = ( lfp (A(),f));

      d is_a_fixpoint_of f by Th4;

      then d = (f . d);

      hence F(d) = d by A3;

      thus thesis;

    end;

    reserve X,Y for non empty set,

f for Function of X, Y,

g for Function of Y, X;

    theorem :: KNASTER:9

    

     Th9: ex Xa,Xb,Ya,Yb be set st Xa misses Xb & Ya misses Yb & (Xa \/ Xb) = X & (Ya \/ Yb) = Y & (f .: Xa) = Ya & (g .: Yb) = Xb

    proof

      deffunc F( set) = (X \ (g .: (Y \ (f .: $1))));

      

       A1: for x be set st x in ( bool X) holds F(x) in ( bool X);

      consider h be Function of ( bool X), ( bool X) such that

       A2: for x be set st x in ( bool X) holds (h . x) = F(x) from FUNCT_2:sch 11( A1);

      now

        let x,y be set;

        assume that

         A3: x in ( dom h) and

         A4: y in ( dom h) and

         A5: x c= y;

        (f .: x) c= (f .: y) by A5, RELAT_1: 123;

        then (Y \ (f .: y)) c= (Y \ (f .: x)) by XBOOLE_1: 34;

        then (g .: (Y \ (f .: y))) c= (g .: (Y \ (f .: x))) by RELAT_1: 123;

        then (X \ (g .: (Y \ (f .: x)))) c= (X \ (g .: (Y \ (f .: y)))) by XBOOLE_1: 34;

        then (h . x) c= (X \ (g .: (Y \ (f .: y)))) by A2, A3;

        hence (h . x) c= (h . y) by A2, A4;

      end;

      then

      reconsider h as c=-monotone Function of ( bool X), ( bool X) by COHSP_1:def 11;

      take Xa = ( lfp (X,h));

      take Xb = (X \ Xa);

      take Ya = (f .: Xa);

      take Yb = (Y \ Ya);

      thus Xa misses Xb by XBOOLE_1: 79;

      thus Ya misses Yb by XBOOLE_1: 79;

      thus (Xa \/ Xb) = X by XBOOLE_1: 45;

      thus (Ya \/ Yb) = Y by XBOOLE_1: 45;

      thus (f .: Xa) = Ya;

      

       A6: Xa is_a_fixpoint_of h by Th4;

      

      thus (g .: Yb) = (X /\ (g .: (Y \ (f .: Xa)))) by XBOOLE_1: 28

      .= (X \ (X \ (g .: (Y \ (f .: Xa))))) by XBOOLE_1: 48

      .= (X \ (h . Xa)) by A2

      .= Xb by A6;

    end;

    ::$Notion-Name

    theorem :: KNASTER:10

    

     Th10: for X,Y be non empty set, f be Function of X, Y, g be Function of Y, X st f is one-to-one & g is one-to-one holds ex h be Function of X, Y st h is bijective

    proof

      let X,Y be non empty set, f be Function of X, Y, g be Function of Y, X;

      assume that

       A1: f is one-to-one and

       A2: g is one-to-one;

      consider Xa,Xb,Ya,Yb be set such that

       A3: Xa misses Xb and

       A4: Ya misses Yb and

       A5: (Xa \/ Xb) = X and

       A6: (Ya \/ Yb) = Y and

       A7: (f .: Xa) = Ya and

       A8: (g .: Yb) = Xb by Th9;

      set gYb = (g | Yb);

      

       A9: gYb is one-to-one by A2, FUNCT_1: 52;

      set fXa = (f | Xa);

      ( dom f) = X by FUNCT_2:def 1;

      then

       A10: ( dom fXa) = Xa by A5, RELAT_1: 62, XBOOLE_1: 7;

      set h = (fXa +* (gYb " ));

      ( rng gYb) = Xb by A8, RELAT_1: 115;

      then

       A11: ( dom (gYb " )) = Xb by A9, FUNCT_1: 32;

      then

       A12: X = ( dom h) by A5, A10, FUNCT_4:def 1;

      

       A13: ( rng fXa) = Ya by A7, RELAT_1: 115;

      ( dom g) = Y by FUNCT_2:def 1;

      then ( dom gYb) = Yb by A6, RELAT_1: 62, XBOOLE_1: 7;

      then

       A14: ( rng (gYb " )) = Yb by A9, FUNCT_1: 33;

      (fXa \/ (gYb " )) = h by A3, A10, A11, FUNCT_4: 31;

      then

       A15: ( rng h) = Y by A6, A13, A14, RELAT_1: 12;

      then

      reconsider h as Function of X, Y by A12, FUNCT_2:def 1, RELSET_1: 4;

      

       A16: h is onto by A15, FUNCT_2:def 3;

      take h;

      fXa is one-to-one by A1, FUNCT_1: 52;

      then h is one-to-one by A4, A13, A9, A14, FUNCT_4: 92;

      hence thesis by A16, FUNCT_2:def 4;

    end;

    theorem :: KNASTER:11

    

     Th11: f is bijective implies (X,Y) are_equipotent

    proof

      assume

       A1: f is bijective;

      take h = f;

      

       A2: h is one-to-one onto by A1, FUNCT_2:def 4;

      then

       A3: ( rng h) = Y by FUNCT_2:def 3;

      hereby

        let x be object;

        assume

         A4: x in X;

        reconsider y = (h . x) as object;

        take y;

        thus y in Y by A3, A4, FUNCT_2: 4;

        x in ( dom h) by A4, FUNCT_2:def 1;

        hence [x, y] in h by FUNCT_1: 1;

      end;

      hereby

        let y be object;

        assume y in Y;

        then

        consider x be object such that

         A5: x in ( dom h) & y = (h . x) by A3, FUNCT_1:def 3;

        reconsider x as object;

        take x;

        thus x in X & [x, y] in h by A5, FUNCT_1: 1;

      end;

      let x,y,z,u be object;

      assume that

       A6: [x, y] in h and

       A7: [z, u] in h;

      

       A8: z in ( dom h) & u = (h . z) by A7, FUNCT_1: 1;

      x in ( dom h) & y = (h . x) by A6, FUNCT_1: 1;

      hence thesis by A2, A8;

    end;

    theorem :: KNASTER:12

    f is one-to-one & g is one-to-one implies (X,Y) are_equipotent

    proof

      assume f is one-to-one & g is one-to-one;

      then ex h be Function of X, Y st h is bijective by Th10;

      hence thesis by Th11;

    end;

    begin

    definition

      let L be Lattice, f be Function of the carrier of L, the carrier of L, x be Element of L, O be Ordinal;

      :: KNASTER:def4

      func (f,O) +. x -> set means

      : Def4: ex L0 be Sequence st it = ( last L0) & ( dom L0) = ( succ O) & (L0 . 0 ) = x & (for C be Ordinal st ( succ C) in ( succ O) holds (L0 . ( succ C)) = (f . (L0 . C))) & for C be Ordinal st C in ( succ O) & C <> 0 & C is limit_ordinal holds (L0 . C) = ( "\/" (( rng (L0 | C)),L));

      correctness

      proof

        deffunc D( Ordinal, Sequence) = ( "\/" (( rng $2),L));

        deffunc C( Ordinal, set) = (f . $2);

        (ex z be object, S be Sequence st z = ( last S) & ( dom S) = ( succ O) & (S . 0 ) = x & (for C be Ordinal st ( succ C) in ( succ O) holds (S . ( succ C)) = C(C,.)) & for C be Ordinal st C in ( succ O) & C <> 0 & C is limit_ordinal holds (S . C) = D(C,|)) & for x1,x2 be set st (ex L0 be Sequence st x1 = ( last L0) & ( dom L0) = ( succ O) & (L0 . 0 ) = x & (for C be Ordinal st ( succ C) in ( succ O) holds (L0 . ( succ C)) = C(C,.)) & for C be Ordinal st C in ( succ O) & C <> 0 & C is limit_ordinal holds (L0 . C) = D(C,|)) & (ex L0 be Sequence st x2 = ( last L0) & ( dom L0) = ( succ O) & (L0 . 0 ) = x & (for C be Ordinal st ( succ C) in ( succ O) holds (L0 . ( succ C)) = C(C,.)) & for C be Ordinal st C in ( succ O) & C <> 0 & C is limit_ordinal holds (L0 . C) = D(C,|)) holds x1 = x2 from ORDINAL2:sch 7;

        hence thesis;

      end;

      :: KNASTER:def5

      func (f,O) -. x -> set means

      : Def5: ex L0 be Sequence st it = ( last L0) & ( dom L0) = ( succ O) & (L0 . 0 ) = x & (for C be Ordinal st ( succ C) in ( succ O) holds (L0 . ( succ C)) = (f . (L0 . C))) & for C be Ordinal st C in ( succ O) & C <> 0 & C is limit_ordinal holds (L0 . C) = ( "/\" (( rng (L0 | C)),L));

      correctness

      proof

        deffunc D( Ordinal, Sequence) = ( "/\" (( rng $2),L));

        deffunc C( Ordinal, set) = (f . $2);

        (ex z be object, S be Sequence st z = ( last S) & ( dom S) = ( succ O) & (S . 0 ) = x & (for C be Ordinal st ( succ C) in ( succ O) holds (S . ( succ C)) = C(C,.)) & for C be Ordinal st C in ( succ O) & C <> 0 & C is limit_ordinal holds (S . C) = D(C,|)) & for x1,x2 be set st (ex L0 be Sequence st x1 = ( last L0) & ( dom L0) = ( succ O) & (L0 . 0 ) = x & (for C be Ordinal st ( succ C) in ( succ O) holds (L0 . ( succ C)) = C(C,.)) & for C be Ordinal st C in ( succ O) & C <> 0 & C is limit_ordinal holds (L0 . C) = D(C,|)) & (ex L0 be Sequence st x2 = ( last L0) & ( dom L0) = ( succ O) & (L0 . 0 ) = x & (for C be Ordinal st ( succ C) in ( succ O) holds (L0 . ( succ C)) = C(C,.)) & for C be Ordinal st C in ( succ O) & C <> 0 & C is limit_ordinal holds (L0 . C) = D(C,|)) holds x1 = x2 from ORDINAL2:sch 7;

        hence thesis;

      end;

    end

    reserve L for Lattice,

f for Function of the carrier of L, the carrier of L,

x for Element of L,

O,O1,O2,O3,O4 for Ordinal,

T for Sequence;

    theorem :: KNASTER:13

    

     Th13: ((f, 0 ) +. x) = x

    proof

      deffunc C( Ordinal, set) = (f . $2);

      deffunc D( Ordinal, Sequence) = ( "\/" (( rng $2),L));

      deffunc F( Ordinal) = ((f,$1) +. x);

      

       A1: for O be Ordinal, y be object holds y = F(O) iff ex L0 be Sequence st y = ( last L0) & ( dom L0) = ( succ O) & (L0 . 0 ) = x & (for C be Ordinal st ( succ C) in ( succ O) holds (L0 . ( succ C)) = C(C,.)) & for C be Ordinal st C in ( succ O) & C <> 0 & C is limit_ordinal holds (L0 . C) = D(C,|) by Def4;

      thus F(0) = x from ORDINAL2:sch 8( A1);

    end;

    theorem :: KNASTER:14

    

     Th14: ((f, 0 ) -. x) = x

    proof

      deffunc C( Ordinal, set) = (f . $2);

      deffunc D( Ordinal, Sequence) = ( "/\" (( rng $2),L));

      deffunc F( Ordinal) = ((f,$1) -. x);

      

       A1: for O be Ordinal, y be object holds y = F(O) iff ex L0 be Sequence st y = ( last L0) & ( dom L0) = ( succ O) & (L0 . 0 ) = x & (for C be Ordinal st ( succ C) in ( succ O) holds (L0 . ( succ C)) = C(C,.)) & for C be Ordinal st C in ( succ O) & C <> 0 & C is limit_ordinal holds (L0 . C) = D(C,|) by Def5;

      thus F(0) = x from ORDINAL2:sch 8( A1);

    end;

    theorem :: KNASTER:15

    

     Th15: ((f,( succ O)) +. x) = (f . ((f,O) +. x))

    proof

      deffunc C( Ordinal, set) = (f . $2);

      deffunc D( Ordinal, Sequence) = ( "\/" (( rng $2),L));

      deffunc F( Ordinal) = ((f,$1) +. x);

      

       A1: for O be Ordinal, y be object holds y = F(O) iff ex L0 be Sequence st y = ( last L0) & ( dom L0) = ( succ O) & (L0 . 0 ) = x & (for C be Ordinal st ( succ C) in ( succ O) holds (L0 . ( succ C)) = C(C,.)) & for C be Ordinal st C in ( succ O) & C <> 0 & C is limit_ordinal holds (L0 . C) = D(C,|) by Def4;

      for O be Ordinal holds F(succ) = C(O,F) from ORDINAL2:sch 9( A1);

      hence thesis;

    end;

    theorem :: KNASTER:16

    

     Th16: ((f,( succ O)) -. x) = (f . ((f,O) -. x))

    proof

      deffunc C( Ordinal, set) = (f . $2);

      deffunc D( Ordinal, Sequence) = ( "/\" (( rng $2),L));

      deffunc F( Ordinal) = ((f,$1) -. x);

      

       A1: for O be Ordinal, y be object holds y = F(O) iff ex L0 be Sequence st y = ( last L0) & ( dom L0) = ( succ O) & (L0 . 0 ) = x & (for C be Ordinal st ( succ C) in ( succ O) holds (L0 . ( succ C)) = C(C,.)) & for C be Ordinal st C in ( succ O) & C <> 0 & C is limit_ordinal holds (L0 . C) = D(C,|) by Def5;

      for O be Ordinal holds F(succ) = C(O,F) from ORDINAL2:sch 9( A1);

      hence thesis;

    end;

    theorem :: KNASTER:17

    

     Th17: O <> 0 & O is limit_ordinal & ( dom T) = O & (for A be Ordinal st A in O holds (T . A) = ((f,A) +. x)) implies ((f,O) +. x) = ( "\/" (( rng T),L))

    proof

      deffunc C( Ordinal, set) = (f . $2);

      deffunc D( Ordinal, Sequence) = ( "\/" (( rng $2),L));

      deffunc F( Ordinal) = ((f,$1) +. x);

      assume that

       A1: O <> 0 & O is limit_ordinal and

       A2: ( dom T) = O and

       A3: for A be Ordinal st A in O holds (T . A) = F(A);

      

       A4: for O be Ordinal, y be object holds y = F(O) iff ex L0 be Sequence st y = ( last L0) & ( dom L0) = ( succ O) & (L0 . 0 ) = x & (for C be Ordinal st ( succ C) in ( succ O) holds (L0 . ( succ C)) = C(C,.)) & for C be Ordinal st C in ( succ O) & C <> 0 & C is limit_ordinal holds (L0 . C) = D(C,|) by Def4;

      thus F(O) = D(O,T) from ORDINAL2:sch 10( A4, A1, A2, A3);

    end;

    theorem :: KNASTER:18

    

     Th18: O <> 0 & O is limit_ordinal & ( dom T) = O & (for A be Ordinal st A in O holds (T . A) = ((f,A) -. x)) implies ((f,O) -. x) = ( "/\" (( rng T),L))

    proof

      deffunc C( Ordinal, set) = (f . $2);

      deffunc D( Ordinal, Sequence) = ( "/\" (( rng $2),L));

      deffunc F( Ordinal) = ((f,$1) -. x);

      assume that

       A1: O <> 0 & O is limit_ordinal and

       A2: ( dom T) = O and

       A3: for A be Ordinal st A in O holds (T . A) = F(A);

      

       A4: for O be Ordinal, y be object holds y = F(O) iff ex L0 be Sequence st y = ( last L0) & ( dom L0) = ( succ O) & (L0 . 0 ) = x & (for C be Ordinal st ( succ C) in ( succ O) holds (L0 . ( succ C)) = C(C,.)) & for C be Ordinal st C in ( succ O) & C <> 0 & C is limit_ordinal holds (L0 . C) = D(C,|) by Def5;

      thus F(O) = D(O,T) from ORDINAL2:sch 10( A4, A1, A2, A3);

    end;

    theorem :: KNASTER:19

    (( iter (f,n)) . x) = ((f,n) +. x)

    proof

      defpred P[ Nat] means (( iter (f,$1)) . x) = ((f,$1) +. x);

      

       A1: ( dom f) = the carrier of L by FUNCT_2:def 1;

      then

       A2: x in ( field f) by XBOOLE_0:def 3;

       A3:

      now

        let n be Nat;

        assume

         A4: P[n];

        ( rng f) c= the carrier of L;

        then

         A5: ( dom ( iter (f,n))) = ( dom f) by A1, FUNCT_7: 74;

        (( iter (f,(n + 1))) . x) = ((f * ( iter (f,n))) . x) by FUNCT_7: 71

        .= (f . ((f,n) +. x)) by A1, A4, A5, FUNCT_1: 13

        .= ((f,( succ ( Segm n))) +. x) by Th15

        .= ((f,( Segm (n + 1))) +. x) by NAT_1: 38;

        hence P[(n + 1)];

      end;

      (( iter (f, 0 )) . x) = (( id ( field f)) . x) by FUNCT_7: 68

      .= x by A2, FUNCT_1: 18

      .= ((f, 0 ) +. x) by Th13;

      then

       A6: P[ 0 ];

      for n be Nat holds P[n] from NAT_1:sch 2( A6, A3);

      hence thesis;

    end;

    theorem :: KNASTER:20

    (( iter (f,n)) . x) = ((f,n) -. x)

    proof

      defpred P[ Nat] means (( iter (f,$1)) . x) = ((f,$1) -. x);

      

       A1: ( dom f) = the carrier of L by FUNCT_2:def 1;

      then

       A2: x in ( field f) by XBOOLE_0:def 3;

       A3:

      now

        let n be Nat;

        assume

         A4: P[n];

        ( rng f) c= the carrier of L;

        then

         A5: ( dom ( iter (f,n))) = ( dom f) by A1, FUNCT_7: 74;

        (( iter (f,(n + 1))) . x) = ((f * ( iter (f,n))) . x) by FUNCT_7: 71

        .= (f . ((f,n) -. x)) by A1, A4, A5, FUNCT_1: 13

        .= ((f,( succ ( Segm n))) -. x) by Th16

        .= ((f,( Segm (n + 1))) -. x) by NAT_1: 38;

        hence P[(n + 1)];

      end;

      (( iter (f, 0 )) . x) = (( id ( field f)) . x) by FUNCT_7: 68

      .= x by A2, FUNCT_1: 18

      .= ((f, 0 ) -. x) by Th14;

      then

       A6: P[ 0 ];

      for n be Nat holds P[n] from NAT_1:sch 2( A6, A3);

      hence thesis;

    end;

    definition

      let L be Lattice, f be UnOp of the carrier of L, a be Element of L, O be Ordinal;

      :: original: +.

      redefine

      func (f,O) +. a -> Element of L ;

      coherence

      proof

        deffunc F( Ordinal) = ((f,$1) +. a);

        defpred P[ Ordinal] means ((f,$1) +. a) is Element of L;

         A1:

        now

          let O1;

          assume P[O1];

          then

          reconsider fa = ((f,O1) +. a) as Element of L;

          (f . fa) = ((f,( succ O1)) +. a) by Th15;

          hence P[( succ O1)];

        end;

         A2:

        now

          let O1;

          assume that

           A3: O1 <> 0 & O1 is limit_ordinal and for O2 st O2 in O1 holds P[O2];

          consider Ls be Sequence such that

           A4: ( dom Ls) = O1 & for O2 be Ordinal st O2 in O1 holds (Ls . O2) = F(O2) from ORDINAL2:sch 2;

          ((f,O1) +. a) = ( "\/" (( rng Ls),L)) by A3, A4, Th17;

          hence P[O1];

        end;

        

         A5: P[ 0 ] by Th13;

        for O holds P[O] from ORDINAL2:sch 1( A5, A1, A2);

        hence thesis;

      end;

    end

    definition

      let L be Lattice, f be UnOp of the carrier of L, a be Element of L, O be Ordinal;

      :: original: -.

      redefine

      func (f,O) -. a -> Element of L ;

      coherence

      proof

        deffunc F( Ordinal) = ((f,$1) -. a);

        defpred P[ Ordinal] means ((f,$1) -. a) is Element of L;

         A1:

        now

          let O1;

          assume P[O1];

          then

          reconsider fa = ((f,O1) -. a) as Element of L;

          (f . fa) = ((f,( succ O1)) -. a) by Th16;

          hence P[( succ O1)];

        end;

         A2:

        now

          let O1;

          assume that

           A3: O1 <> 0 & O1 is limit_ordinal and for O2 st O2 in O1 holds P[O2];

          consider Ls be Sequence such that

           A4: ( dom Ls) = O1 & for O2 be Ordinal st O2 in O1 holds (Ls . O2) = F(O2) from ORDINAL2:sch 2;

          ((f,O1) -. a) = ( "/\" (( rng Ls),L)) by A3, A4, Th18;

          hence P[O1];

        end;

        

         A5: P[ 0 ] by Th14;

        for O holds P[O] from ORDINAL2:sch 1( A5, A1, A2);

        hence thesis;

      end;

    end

    definition

      let L be non empty LattStr, P be Subset of L;

      :: KNASTER:def6

      attr P is with_suprema means

      : Def6: for x,y be Element of L st x in P & y in P holds ex z be Element of L st z in P & x [= z & y [= z & for z9 be Element of L st z9 in P & x [= z9 & y [= z9 holds z [= z9;

      :: KNASTER:def7

      attr P is with_infima means

      : Def7: for x,y be Element of L st x in P & y in P holds ex z be Element of L st z in P & z [= x & z [= y & for z9 be Element of L st z9 in P & z9 [= x & z9 [= y holds z9 [= z;

    end

    registration

      let L be Lattice;

      cluster non empty with_suprema with_infima for Subset of L;

      existence

      proof

        the carrier of L c= the carrier of L;

        then

        reconsider P = the carrier of L as Subset of L;

        take P;

        thus P is non empty;

        thus P is with_suprema

        proof

          let x,y be Element of L such that x in P and y in P;

          take z = (x "\/" y);

          thus z in P;

          thus x [= z & y [= z by LATTICES: 5;

          let z9 be Element of L;

          assume that z9 in P and

           A1: x [= z9 & y [= z9;

          thus z [= z9 by A1, BOOLEALG: 5;

        end;

        let x,y be Element of L such that x in P and y in P;

        take z = (x "/\" y);

        thus z in P;

        thus z [= x & z [= y by LATTICES: 6;

        let z9 be Element of L;

        assume that z9 in P and

         A2: z9 [= x & z9 [= y;

        thus z9 [= z by A2, BOOLEALG: 6;

      end;

    end

    definition

      let L be Lattice, P be non empty with_suprema with_infima Subset of L;

      :: KNASTER:def8

      func latt P -> strict Lattice means

      : Def8: the carrier of it = P & for x,y be Element of it holds ex x9,y9 be Element of L st x = x9 & y = y9 & (x [= y iff x9 [= y9);

      existence

      proof

        set cL = the carrier of L;

        set LL = ( LattRel L);

        set LR = (LL |_2 P);

        reconsider LR as Relation of P by XBOOLE_1: 17;

        ( field LL) = cL by FILTER_1: 32;

        then

         A1: LL is_reflexive_in cL by RELAT_2:def 9;

        

         A2: ( field LR) = P

        proof

          thus ( field LR) c= P by WELLORD1: 13;

          let x be object;

          assume x in P;

          then [x, x] in [:P, P:] & [x, x] in LL by A1, RELAT_2:def 1, ZFMISC_1: 87;

          then [x, x] in LR by XBOOLE_0:def 4;

          hence thesis by RELAT_1: 15;

        end;

        LR is reflexive by WELLORD1: 15;

        then

         A3: LR is_reflexive_in P by A2, RELAT_2:def 9;

        then

         A4: ( dom LR) = P by ORDERS_1: 13;

        LR is transitive by WELLORD1: 17;

        then

         A5: LR is_transitive_in P by A2, RELAT_2:def 16;

        LR is antisymmetric by WELLORD1: 18;

        then

         A6: LR is_antisymmetric_in P by A2, RELAT_2:def 12;

        reconsider LR as Order of P by A4, PARTFUN1:def 2, WELLORD1: 15, WELLORD1: 17, WELLORD1: 18;

        set RS = RelStr (# P, LR #);

        take IT = ( latt RS);

        

         A7: RS is with_suprema

        proof

          let x,y be Element of RS;

          x in P & y in P;

          then

          reconsider xL = x, yL = y as Element of L;

          consider zL be Element of L such that

           A8: zL in P and

           A9: xL [= zL and

           A10: yL [= zL and

           A11: for z9 be Element of L st z9 in P & xL [= z9 & yL [= z9 holds zL [= z9 by Def6;

           [yL, zL] in [:P, P:] & [yL, zL] in LL by A8, A10, FILTER_1: 31, ZFMISC_1: 87;

          then

           A12: [yL, zL] in LR by XBOOLE_0:def 4;

          reconsider z = zL as Element of RS by A8;

          take z;

           [xL, zL] in [:P, P:] & [xL, zL] in LL by A8, A9, FILTER_1: 31, ZFMISC_1: 87;

          then [xL, zL] in LR by XBOOLE_0:def 4;

          hence x <= z & y <= z by A12, ORDERS_2:def 5;

          let z9 be Element of RS;

          assume that

           A13: x <= z9 and

           A14: y <= z9;

          z9 in P;

          then

          reconsider z9L = z9 as Element of L;

           [y, z9] in LR by A14, ORDERS_2:def 5;

          then [y, z9] in LL by XBOOLE_0:def 4;

          then

           A15: yL [= z9L by FILTER_1: 31;

           [x, z9] in LR by A13, ORDERS_2:def 5;

          then [x, z9] in LL by XBOOLE_0:def 4;

          then xL [= z9L by FILTER_1: 31;

          then zL [= z9L by A11, A15;

          then

           A16: [zL, z9L] in LL by FILTER_1: 31;

           [zL, z9L] in [:P, P:] by A8, ZFMISC_1: 87;

          then [zL, z9L] in LR by A16, XBOOLE_0:def 4;

          hence thesis by ORDERS_2:def 5;

        end;

        

         A17: RS is with_infima

        proof

          let x,y be Element of RS;

          x in P & y in P;

          then

          reconsider xL = x, yL = y as Element of L;

          consider zL be Element of L such that

           A18: zL in P and

           A19: zL [= xL and

           A20: zL [= yL and

           A21: for z9 be Element of L st z9 in P & z9 [= xL & z9 [= yL holds z9 [= zL by Def7;

           [zL, yL] in [:P, P:] & [zL, yL] in LL by A18, A20, FILTER_1: 31, ZFMISC_1: 87;

          then

           A22: [zL, yL] in LR by XBOOLE_0:def 4;

          reconsider z = zL as Element of RS by A18;

          take z;

           [zL, xL] in [:P, P:] & [zL, xL] in LL by A18, A19, FILTER_1: 31, ZFMISC_1: 87;

          then [zL, xL] in LR by XBOOLE_0:def 4;

          hence z <= x & z <= y by A22, ORDERS_2:def 5;

          let z9 be Element of RS;

          assume that

           A23: z9 <= x and

           A24: z9 <= y;

          z9 in P;

          then

          reconsider z9L = z9 as Element of L;

           [z9, y] in LR by A24, ORDERS_2:def 5;

          then [z9, y] in LL by XBOOLE_0:def 4;

          then

           A25: z9L [= yL by FILTER_1: 31;

           [z9, x] in LR by A23, ORDERS_2:def 5;

          then [z9, x] in LL by XBOOLE_0:def 4;

          then z9L [= xL by FILTER_1: 31;

          then z9L [= zL by A21, A25;

          then

           A26: [z9L, zL] in LL by FILTER_1: 31;

           [z9L, zL] in [:P, P:] by A18, ZFMISC_1: 87;

          then [z9L, zL] in LR by A26, XBOOLE_0:def 4;

          hence thesis by ORDERS_2:def 5;

        end;

        

         A27: RS is Poset by A3, A6, A5, ORDERS_2:def 2, ORDERS_2:def 3, ORDERS_2:def 4;

        then

         A28: RS = ( LattPOSet IT) by A7, A17, LATTICE3:def 15;

        ( LattPOSet IT) = RelStr (# the carrier of IT, ( LattRel IT) #);

        hence the carrier of IT = P by A7, A17, A27, LATTICE3:def 15;

        let x,y be Element of IT;

        x in P & y in P by A28;

        then

        reconsider x9 = x, y9 = y as Element of L;

        take x9, y9;

        thus x = x9 & y = y9;

        hereby

          assume x [= y;

          then [x, y] in LR by A28, FILTER_1: 31;

          then [x, y] in ( LattRel L) by XBOOLE_0:def 4;

          hence x9 [= y9 by FILTER_1: 31;

        end;

        assume x9 [= y9;

        then

         A29: [x, y] in ( LattRel L) by FILTER_1: 31;

         [x, y] in [:P, P:] by A28, ZFMISC_1: 87;

        then [x, y] in ( LattRel IT) by A28, A29, XBOOLE_0:def 4;

        hence thesis by FILTER_1: 31;

      end;

      uniqueness

      proof

        let it1,it2 be strict Lattice such that

         A30: the carrier of it1 = P and

         A31: for x,y be Element of it1 holds ex x9,y9 be Element of L st x = x9 & y = y9 & (x [= y iff x9 [= y9) and

         A32: the carrier of it2 = P and

         A33: for x,y be Element of it2 holds ex x9,y9 be Element of L st x = x9 & y = y9 & (x [= y iff x9 [= y9);

        

         A34: ( LattRel it2) = { [p, q] where p be Element of it2, q be Element of it2 : p [= q } by FILTER_1:def 8;

        

         A35: ( LattRel it1) = { [p, q] where p be Element of it1, q be Element of it1 : p [= q } by FILTER_1:def 8;

        now

          let a be object;

          hereby

            assume a in ( LattRel it1);

            then

            consider p1,q1 be Element of it1 such that

             A36: a = [p1, q1] & p1 [= q1 by A35;

            reconsider p1, q1 as Element of it1;

            reconsider p2 = p1, q2 = q1 as Element of it2 by A30, A32;

            (ex pl1,ql1 be Element of L st p1 = pl1 & q1 = ql1 & (p1 [= q1 iff pl1 [= ql1)) & ex pl2,ql2 be Element of L st p2 = pl2 & q2 = ql2 & (p2 [= q2 iff pl2 [= ql2) by A31, A33;

            hence a in ( LattRel it2) by A34, A36;

          end;

          assume a in ( LattRel it2);

          then

          consider p1,q1 be Element of it2 such that

           A37: a = [p1, q1] & p1 [= q1 by A34;

          reconsider p1, q1 as Element of it2;

          reconsider p2 = p1, q2 = q1 as Element of it1 by A30, A32;

          (ex pl1,ql1 be Element of L st p1 = pl1 & q1 = ql1 & (p1 [= q1 iff pl1 [= ql1)) & ex pl2,ql2 be Element of L st p2 = pl2 & q2 = ql2 & (p2 [= q2 iff pl2 [= ql2) by A31, A33;

          hence a in ( LattRel it1) by A35, A37;

        end;

        then

         A38: ( LattRel it1) = ( LattRel it2);

        ( LattPOSet it1) = RelStr (# the carrier of it1, ( LattRel it1) #) & ( LattPOSet it2) = RelStr (# the carrier of it2, ( LattRel it2) #);

        hence thesis by A30, A32, A38, LATTICE3: 6;

      end;

    end

    begin

    registration

      cluster complete -> bounded for Lattice;

      coherence

      proof

        let L be Lattice;

        assume L is complete;

        then L is 0_Lattice & L is 1_Lattice by LATTICE3: 49, LATTICE3: 50;

        hence thesis;

      end;

    end

    reserve L for complete Lattice,

f for monotone UnOp of L,

a,b for Element of L;

    theorem :: KNASTER:21

    

     Th21: ex a st a is_a_fixpoint_of f

    proof

      set H = { h where h be Element of L : h [= (f . h) };

      set fH = { (f . h) where h be Element of L : h [= (f . h) };

      set uH = ( "\/" (H,L));

      set fuH = ( "\/" (fH,L));

      take uH;

      now

        let fh be Element of L;

        assume fh in fH;

        then

        consider h be Element of L such that

         A1: fh = (f . h) and

         A2: h [= (f . h);

        h in H by A2;

        then h [= uH by LATTICE3: 38;

        hence fh [= (f . uH) by A1, QUANTAL1:def 12;

      end;

      then fH is_less_than (f . uH);

      then

       A3: fuH [= (f . uH) by LATTICE3:def 21;

      now

        let a be Element of L;

        assume a in H;

        then

        consider h be Element of L such that

         A4: a = h & h [= (f . h);

        reconsider fh = (f . h) as Element of L;

        take fh;

        thus a [= fh & fh in fH by A4;

      end;

      then uH [= fuH by LATTICE3: 47;

      then

       A5: uH [= (f . uH) by A3, LATTICES: 7;

      then (f . uH) [= (f . (f . uH)) by QUANTAL1:def 12;

      then (f . uH) in H;

      then (f . uH) [= uH by LATTICE3: 38;

      hence uH = (f . uH) by A5, LATTICES: 8;

    end;

    theorem :: KNASTER:22

    

     Th22: for a st a [= (f . a) holds for O holds a [= ((f,O) +. a)

    proof

      let a;

      defpred S[ Ordinal] means a [= ((f,$1) +. a);

      deffunc F( Ordinal) = ((f,$1) +. a);

       A1:

      now

        let O1;

        assume that

         A2: O1 <> 0 and

         A3: O1 is limit_ordinal and

         A4: for O2 st O2 in O1 holds S[O2];

        consider O2 be object such that

         A5: O2 in O1 by A2, XBOOLE_0:def 1;

        reconsider O2 as Ordinal by A5;

        

         A6: S[O2] by A4, A5;

        consider Ls be Sequence such that

         A7: ( dom Ls) = O1 & for O2 be Ordinal st O2 in O1 holds (Ls . O2) = F(O2) from ORDINAL2:sch 2;

        (Ls . O2) = ((f,O2) +. a) & (Ls . O2) in ( rng Ls) by A7, A5, FUNCT_1:def 3;

        then ((f,O2) +. a) [= ( "\/" (( rng Ls),L)) by LATTICE3: 38;

        then a [= ( "\/" (( rng Ls),L)) by A6, LATTICES: 7;

        hence S[O1] by A2, A3, A7, Th17;

      end;

      assume

       A8: a [= (f . a);

       A9:

      now

        let O1;

        assume S[O1];

        then (f . a) [= (f . ((f,O1) +. a)) by QUANTAL1:def 12;

        then a [= (f . ((f,O1) +. a)) by A8, LATTICES: 7;

        hence S[( succ O1)] by Th15;

      end;

      

       A10: S[ 0 ] by Th13;

      thus for O holds S[O] from ORDINAL2:sch 1( A10, A9, A1);

    end;

    theorem :: KNASTER:23

    

     Th23: for a st (f . a) [= a holds for O holds ((f,O) -. a) [= a

    proof

      let a;

      defpred S[ Ordinal] means ((f,$1) -. a) [= a;

      deffunc F( Ordinal) = ((f,$1) -. a);

       A1:

      now

        let O1;

        assume that

         A2: O1 <> 0 and

         A3: O1 is limit_ordinal and

         A4: for O2 st O2 in O1 holds S[O2];

        consider O2 be object such that

         A5: O2 in O1 by A2, XBOOLE_0:def 1;

        reconsider O2 as Ordinal by A5;

        

         A6: S[O2] by A4, A5;

        consider Ls be Sequence such that

         A7: ( dom Ls) = O1 & for O2 be Ordinal st O2 in O1 holds (Ls . O2) = F(O2) from ORDINAL2:sch 2;

        (Ls . O2) = ((f,O2) -. a) & (Ls . O2) in ( rng Ls) by A7, A5, FUNCT_1:def 3;

        then ( "/\" (( rng Ls),L)) [= ((f,O2) -. a) by LATTICE3: 38;

        then ( "/\" (( rng Ls),L)) [= a by A6, LATTICES: 7;

        hence S[O1] by A2, A3, A7, Th18;

      end;

      assume

       A8: (f . a) [= a;

       A9:

      now

        let O1;

        assume S[O1];

        then (f . ((f,O1) -. a)) [= (f . a) by QUANTAL1:def 12;

        then (f . ((f,O1) -. a)) [= a by A8, LATTICES: 7;

        hence S[( succ O1)] by Th16;

      end;

      

       A10: S[ 0 ] by Th14;

      thus for O holds S[O] from ORDINAL2:sch 1( A10, A9, A1);

    end;

    theorem :: KNASTER:24

    

     Th24: for a st a [= (f . a) holds for O1, O2 st O1 c= O2 holds ((f,O1) +. a) [= ((f,O2) +. a)

    proof

      let a;

      defpred S[ Ordinal] means for O1, O2 st O1 c= O2 & O2 c= $1 holds ((f,O1) +. a) [= ((f,O2) +. a);

       A1:

      now

        let O4;

        assume that

         A2: O4 <> 0 & O4 is limit_ordinal and

         A3: for O3 st O3 in O4 holds S[O3];

        thus S[O4]

        proof

          let O1, O2;

          assume that

           A4: O1 c= O2 and

           A5: O2 c= O4;

          

           A6: O2 c< O4 iff O2 c= O4 & O2 <> O4;

          

           A7: O1 c< O2 iff O1 c= O2 & O1 <> O2;

          per cases by A5, A6, ORDINAL1: 11;

            suppose

             A8: O2 = O4;

            thus ((f,O1) +. a) [= ((f,O2) +. a)

            proof

              per cases by A4, A7, ORDINAL1: 11;

                suppose O1 = O2;

                hence thesis;

              end;

                suppose

                 A9: O1 in O2;

                deffunc F( Ordinal) = ((f,$1) +. a);

                consider L1 be Sequence such that

                 A10: ( dom L1) = O2 & for O3 st O3 in O2 holds (L1 . O3) = F(O3) from ORDINAL2:sch 2;

                

                 A11: (L1 . O1) = ((f,O1) +. a) & (L1 . O1) in ( rng L1) by A9, A10, FUNCT_1:def 3;

                ((f,O2) +. a) = ( "\/" (( rng L1),L)) by A2, A8, A10, Th17;

                hence thesis by A11, LATTICE3: 38;

              end;

            end;

          end;

            suppose O2 in O4;

            hence thesis by A3, A4;

          end;

        end;

      end;

      assume

       A12: a [= (f . a);

       A13:

      now

        let O4;

        assume

         A14: S[O4];

        thus S[( succ O4)]

        proof

          let O1, O2;

          assume that

           A15: O1 c= O2 and

           A16: O2 c= ( succ O4);

          per cases ;

            suppose O1 = O2 & O2 <> ( succ O4);

            hence thesis;

          end;

            suppose O1 <> O2 & O2 <> ( succ O4);

            then O2 c< ( succ O4) by A16;

            then O2 in ( succ O4) by ORDINAL1: 11;

            then O2 c= O4 by ORDINAL1: 22;

            hence thesis by A14, A15;

          end;

            suppose O1 = O2 & O2 = ( succ O4);

            hence thesis;

          end;

            suppose

             A17: O1 <> O2 & O2 = ( succ O4);

            

             A18: ((f,O4) +. a) [= ((f,( succ O4)) +. a)

            proof

              per cases by ORDINAL1: 29;

                suppose

                 A19: O4 is limit_ordinal;

                thus thesis

                proof

                  per cases ;

                    suppose O4 = {} ;

                    then ((f,O4) +. a) = a by Th13;

                    hence thesis by A12, Th15;

                  end;

                    suppose

                     A20: O4 <> {} ;

                    deffunc F( Ordinal) = ((f,$1) +. a);

                    consider L1 be Sequence such that

                     A21: ( dom L1) = O4 & for O3 st O3 in O4 holds (L1 . O3) = F(O3) from ORDINAL2:sch 2;

                    

                     A22: ( rng L1) is_less_than ((f,( succ O4)) +. a)

                    proof

                      let q be Element of L;

                      assume q in ( rng L1);

                      then

                      consider O3 be object such that

                       A23: O3 in ( dom L1) and

                       A24: q = (L1 . O3) by FUNCT_1:def 3;

                      reconsider O3 as Ordinal by A23;

                      O3 in ( succ O3) by ORDINAL1: 6;

                      then

                       A25: O3 c= ( succ O3) by ORDINAL1:def 2;

                      O3 c= O4 by A21, A23, ORDINAL1:def 2;

                      then ((f,O3) +. a) [= ((f,O4) +. a) by A14;

                      then (f . ((f,O3) +. a)) [= (f . ((f,O4) +. a)) by QUANTAL1:def 12;

                      then ((f,( succ O3)) +. a) [= (f . ((f,O4) +. a)) by Th15;

                      then

                       A26: ((f,( succ O3)) +. a) [= ((f,( succ O4)) +. a) by Th15;

                      ( succ O3) c= O4 by A21, A23, ORDINAL1: 21;

                      then

                       A27: ((f,O3) +. a) [= ((f,( succ O3)) +. a) by A14, A25;

                      q = ((f,O3) +. a) by A21, A23, A24;

                      hence q [= ((f,( succ O4)) +. a) by A26, A27, LATTICES: 7;

                    end;

                    ((f,O4) +. a) = ( "\/" (( rng L1),L)) by A19, A20, A21, Th17;

                    hence thesis by A22, LATTICE3:def 21;

                  end;

                end;

              end;

                suppose ex O3 st O4 = ( succ O3);

                then

                consider O3 such that

                 A28: O4 = ( succ O3);

                O3 c= O4 by A28, XBOOLE_1: 7;

                then ((f,O3) +. a) [= ((f,O4) +. a) by A14;

                then (f . ((f,O3) +. a)) [= (f . ((f,O4) +. a)) by QUANTAL1:def 12;

                then ((f,O4) +. a) [= (f . ((f,O4) +. a)) by A28, Th15;

                hence thesis by Th15;

              end;

            end;

            O1 c< O2 by A15, A17;

            then O1 in O2 by ORDINAL1: 11;

            then O1 c= O4 by A17, ORDINAL1: 22;

            then ((f,O1) +. a) [= ((f,O4) +. a) by A14;

            hence thesis by A17, A18, LATTICES: 7;

          end;

        end;

      end;

      let O1, O2;

      assume

       A29: O1 c= O2;

      

       A30: S[ 0 ];

      for O4 holds S[O4] from ORDINAL2:sch 1( A30, A13, A1);

      hence thesis by A29;

    end;

    theorem :: KNASTER:25

    

     Th25: for a st (f . a) [= a holds for O1, O2 st O1 c= O2 holds ((f,O2) -. a) [= ((f,O1) -. a)

    proof

      let a;

      defpred S[ Ordinal] means for O1, O2 st O1 c= O2 & O2 c= $1 holds ((f,O2) -. a) [= ((f,O1) -. a);

       A1:

      now

        let O4;

        assume that

         A2: O4 <> 0 & O4 is limit_ordinal and

         A3: for O3 st O3 in O4 holds S[O3];

        thus S[O4]

        proof

          let O1, O2;

          assume that

           A4: O1 c= O2 and

           A5: O2 c= O4;

          

           A6: O2 c< O4 iff O2 c= O4 & O2 <> O4;

          

           A7: O1 c< O2 iff O1 c= O2 & O1 <> O2;

          per cases by A5, A6, ORDINAL1: 11;

            suppose

             A8: O2 = O4;

            thus ((f,O2) -. a) [= ((f,O1) -. a)

            proof

              per cases by A4, A7, ORDINAL1: 11;

                suppose O1 = O2;

                hence thesis;

              end;

                suppose

                 A9: O1 in O2;

                deffunc F( Ordinal) = ((f,$1) -. a);

                consider L1 be Sequence such that

                 A10: ( dom L1) = O2 & for O3 st O3 in O2 holds (L1 . O3) = F(O3) from ORDINAL2:sch 2;

                

                 A11: (L1 . O1) = ((f,O1) -. a) & (L1 . O1) in ( rng L1) by A9, A10, FUNCT_1:def 3;

                ((f,O2) -. a) = ( "/\" (( rng L1),L)) by A2, A8, A10, Th18;

                hence thesis by A11, LATTICE3: 38;

              end;

            end;

          end;

            suppose O2 in O4;

            hence thesis by A3, A4;

          end;

        end;

      end;

      assume

       A12: (f . a) [= a;

       A13:

      now

        let O4;

        assume

         A14: S[O4];

        thus S[( succ O4)]

        proof

          let O1, O2;

          assume that

           A15: O1 c= O2 and

           A16: O2 c= ( succ O4);

          per cases ;

            suppose O1 = O2 & O2 <> ( succ O4);

            hence thesis;

          end;

            suppose O1 <> O2 & O2 <> ( succ O4);

            then O2 c< ( succ O4) by A16;

            then O2 in ( succ O4) by ORDINAL1: 11;

            then O2 c= O4 by ORDINAL1: 22;

            hence thesis by A14, A15;

          end;

            suppose O1 = O2 & O2 = ( succ O4);

            hence thesis;

          end;

            suppose

             A17: O1 <> O2 & O2 = ( succ O4);

            

             A18: ((f,( succ O4)) -. a) [= ((f,O4) -. a)

            proof

              per cases by ORDINAL1: 29;

                suppose

                 A19: O4 is limit_ordinal;

                thus thesis

                proof

                  per cases ;

                    suppose O4 = {} ;

                    then ((f,O4) -. a) = a by Th14;

                    hence thesis by A12, Th16;

                  end;

                    suppose

                     A20: O4 <> {} ;

                    deffunc F( Ordinal) = ((f,$1) -. a);

                    consider L1 be Sequence such that

                     A21: ( dom L1) = O4 & for O3 st O3 in O4 holds (L1 . O3) = F(O3) from ORDINAL2:sch 2;

                    

                     A22: ((f,( succ O4)) -. a) is_less_than ( rng L1)

                    proof

                      let q be Element of L;

                      assume q in ( rng L1);

                      then

                      consider O3 be object such that

                       A23: O3 in ( dom L1) and

                       A24: q = (L1 . O3) by FUNCT_1:def 3;

                      reconsider O3 as Ordinal by A23;

                      O3 in ( succ O3) by ORDINAL1: 6;

                      then

                       A25: O3 c= ( succ O3) by ORDINAL1:def 2;

                      O3 c= O4 by A21, A23, ORDINAL1:def 2;

                      then ((f,O4) -. a) [= ((f,O3) -. a) by A14;

                      then (f . ((f,O4) -. a)) [= (f . ((f,O3) -. a)) by QUANTAL1:def 12;

                      then ((f,( succ O4)) -. a) [= (f . ((f,O3) -. a)) by Th16;

                      then

                       A26: ((f,( succ O4)) -. a) [= ((f,( succ O3)) -. a) by Th16;

                      ( succ O3) c= O4 by A21, A23, ORDINAL1: 21;

                      then

                       A27: ((f,( succ O3)) -. a) [= ((f,O3) -. a) by A14, A25;

                      q = ((f,O3) -. a) by A21, A23, A24;

                      hence ((f,( succ O4)) -. a) [= q by A26, A27, LATTICES: 7;

                    end;

                    ((f,O4) -. a) = ( "/\" (( rng L1),L)) by A19, A20, A21, Th18;

                    hence thesis by A22, LATTICE3: 34;

                  end;

                end;

              end;

                suppose ex O3 st O4 = ( succ O3);

                then

                consider O3 such that

                 A28: O4 = ( succ O3);

                O3 c= O4 by A28, XBOOLE_1: 7;

                then ((f,O4) -. a) [= ((f,O3) -. a) by A14;

                then (f . ((f,O4) -. a)) [= (f . ((f,O3) -. a)) by QUANTAL1:def 12;

                then (f . ((f,O4) -. a)) [= ((f,O4) -. a) by A28, Th16;

                hence thesis by Th16;

              end;

            end;

            O1 c< O2 by A15, A17;

            then O1 in O2 by ORDINAL1: 11;

            then O1 c= O4 by A17, ORDINAL1: 22;

            then ((f,O4) -. a) [= ((f,O1) -. a) by A14;

            hence thesis by A17, A18, LATTICES: 7;

          end;

        end;

      end;

      let O1, O2;

      assume

       A29: O1 c= O2;

      

       A30: S[ 0 ];

      for O4 holds S[O4] from ORDINAL2:sch 1( A30, A13, A1);

      hence thesis by A29;

    end;

    theorem :: KNASTER:26

    

     Th26: for a st a [= (f . a) holds for O1, O2 st O1 c< O2 & not ((f,O2) +. a) is_a_fixpoint_of f holds ((f,O1) +. a) <> ((f,O2) +. a)

    proof

      let a;

      assume

       A1: a [= (f . a);

      let O1, O2;

      

       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);

      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;

    end;

    theorem :: KNASTER:27

    

     Th27: for a st (f . a) [= a holds for O1, O2 st O1 c< O2 & not ((f,O2) -. a) is_a_fixpoint_of f holds ((f,O1) -. a) <> ((f,O2) -. a)

    proof

      let a;

      assume

       A1: (f . a) [= a;

      let O1, O2;

      

       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);

      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;

    end;

    theorem :: KNASTER:28

    

     Th28: a [= (f . a) & ((f,O1) +. a) is_a_fixpoint_of f implies for O2 st O1 c= O2 holds ((f,O1) +. a) = ((f,O2) +. a)

    proof

      assume that

       A1: a [= (f . a) and

       A2: ((f,O1) +. a) is_a_fixpoint_of f;

      set fa = ((f,O1) +. a);

      defpred S[ Ordinal] means O1 c= $1 implies fa = ((f,$1) +. a);

       A3:

      now

        let O2;

        assume that

         A4: O2 <> 0 & O2 is limit_ordinal and

         A5: for O3 st O3 in O2 holds S[O3];

        thus S[O2]

        proof

          assume O1 c= O2;

          then

           A6: fa [= ((f,O2) +. a) by A1, Th24;

          deffunc F( Ordinal) = ((f,$1) +. a);

          consider L1 be Sequence such that

           A7: ( dom L1) = O2 & for O3 st O3 in O2 holds (L1 . O3) = F(O3) from ORDINAL2:sch 2;

          

           A8: ( rng L1) is_less_than fa

          proof

            let q be Element of L;

            assume q in ( rng L1);

            then

            consider O3 be object such that

             A9: O3 in ( dom L1) and

             A10: q = (L1 . O3) by FUNCT_1:def 3;

            reconsider O3 as Ordinal by A9;

            per cases ;

              suppose O1 c= O3;

              then ((f,O3) +. a) [= fa by A5, A7, A9;

              hence q [= fa by A7, A9, A10;

            end;

              suppose O3 c= O1;

              then ((f,O3) +. a) [= fa by A1, Th24;

              hence q [= fa by A7, A9, A10;

            end;

          end;

          ((f,O2) +. a) = ( "\/" (( rng L1),L)) by A4, A7, Th17;

          then ((f,O2) +. a) [= fa by A8, LATTICE3:def 21;

          hence thesis by A6, LATTICES: 8;

        end;

      end;

       A11:

      now

        let O2;

        assume

         A12: S[O2];

        thus S[( succ O2)]

        proof

          assume

           A13: O1 c= ( succ O2);

          per cases ;

            suppose O1 = ( succ O2);

            hence thesis;

          end;

            suppose O1 <> ( succ O2);

            then O1 c< ( succ O2) by A13;

            then O1 in ( succ O2) by ORDINAL1: 11;

            

            hence fa = (f . ((f,O2) +. a)) by A2, A12, ORDINAL1: 22

            .= ((f,( succ O2)) +. a) by Th15;

          end;

        end;

      end;

      

       A14: S[ 0 ];

      thus for O2 holds S[O2] from ORDINAL2:sch 1( A14, A11, A3);

    end;

    theorem :: KNASTER:29

    

     Th29: (f . a) [= a & ((f,O1) -. a) is_a_fixpoint_of f implies for O2 st O1 c= O2 holds ((f,O1) -. a) = ((f,O2) -. a)

    proof

      assume that

       A1: (f . a) [= a and

       A2: ((f,O1) -. a) is_a_fixpoint_of f;

      set fa = ((f,O1) -. a);

      defpred S[ Ordinal] means O1 c= $1 implies fa = ((f,$1) -. a);

       A3:

      now

        let O2;

        assume that

         A4: O2 <> 0 & O2 is limit_ordinal and

         A5: for O3 st O3 in O2 holds S[O3];

        thus S[O2]

        proof

          assume O1 c= O2;

          then

           A6: ((f,O2) -. a) [= fa by A1, Th25;

          deffunc F( Ordinal) = ((f,$1) -. a);

          consider L1 be Sequence such that

           A7: ( dom L1) = O2 & for O3 st O3 in O2 holds (L1 . O3) = F(O3) from ORDINAL2:sch 2;

          

           A8: fa is_less_than ( rng L1)

          proof

            let q be Element of L;

            assume q in ( rng L1);

            then

            consider O3 be object such that

             A9: O3 in ( dom L1) and

             A10: q = (L1 . O3) by FUNCT_1:def 3;

            reconsider O3 as Ordinal by A9;

            per cases ;

              suppose O1 c= O3;

              then fa [= ((f,O3) -. a) by A5, A7, A9;

              hence fa [= q by A7, A9, A10;

            end;

              suppose O3 c= O1;

              then fa [= ((f,O3) -. a) by A1, Th25;

              hence fa [= q by A7, A9, A10;

            end;

          end;

          ((f,O2) -. a) = ( "/\" (( rng L1),L)) by A4, A7, Th18;

          then fa [= ((f,O2) -. a) by A8, LATTICE3: 39;

          hence thesis by A6, LATTICES: 8;

        end;

      end;

       A11:

      now

        let O2;

        assume

         A12: S[O2];

        thus S[( succ O2)]

        proof

          assume

           A13: O1 c= ( succ O2);

          per cases ;

            suppose O1 = ( succ O2);

            hence thesis;

          end;

            suppose O1 <> ( succ O2);

            then O1 c< ( succ O2) by A13;

            then O1 in ( succ O2) by ORDINAL1: 11;

            

            hence fa = (f . ((f,O2) -. a)) by A2, A12, ORDINAL1: 22

            .= ((f,( succ O2)) -. a) by Th16;

          end;

        end;

      end;

      

       A14: S[ 0 ];

      thus for O2 holds S[O2] from ORDINAL2:sch 1( A14, A11, A3);

    end;

    

     Lm1: O1 c< O2 or O1 = O2 or O2 c< O1

    proof

      assume that

       A1: ( not O1 c< O2) & not O1 = O2 and

       A2: not O2 c< O1;

       not O1 c= O2 by A1;

      hence contradiction by A2;

    end;

    theorem :: KNASTER:30

    

     Th30: for a st a [= (f . a) holds ex O st ( card O) c= ( card the carrier of L) & ((f,O) +. a) is_a_fixpoint_of f

    proof

      let a;

      set cL = the carrier of L;

      set ccL = ( card cL);

      set nccL = ( nextcard ccL);

      deffunc F( Ordinal) = ((f,$1) +. a);

      consider Ls be Sequence such that

       A1: ( dom Ls) = nccL & for O2 be Ordinal st O2 in nccL holds (Ls . O2) = F(O2) from ORDINAL2:sch 2;

      assume

       A2: a [= (f . a);

      now

        assume

         A3: for O st O in nccL holds not ((f,O) +. a) is_a_fixpoint_of f;

        

         A4: Ls is one-to-one

        proof

          let x1,x2 be object;

          assume that

           A5: x1 in ( dom Ls) and

           A6: x2 in ( dom Ls) and

           A7: (Ls . x1) = (Ls . x2);

          reconsider x1, x2 as Ordinal by A5, A6;

          

           A8: (Ls . x1) = ((f,x1) +. a) by A1, A5;

          

           A9: (Ls . x2) = ((f,x2) +. a) by A1, A6;

          per cases by Lm1;

            suppose

             A10: x1 c< x2;

             not ((f,x2) +. a) is_a_fixpoint_of f by A1, A3, A6;

            hence thesis by A2, A1, A6, A7, A8, A10, Th26;

          end;

            suppose

             A11: x2 c< x1;

             not ((f,x1) +. a) is_a_fixpoint_of f by A1, A3, A5;

            hence thesis by A2, A1, A5, A7, A9, A11, Th26;

          end;

            suppose x2 = x1;

            hence thesis;

          end;

        end;

        ( rng Ls) c= cL

        proof

          let y be object;

          assume y in ( rng Ls);

          then

          consider x be object such that

           A12: x in ( dom Ls) and

           A13: (Ls . x) = y by FUNCT_1:def 3;

          reconsider x as Ordinal by A12;

          (Ls . x) = ((f,x) +. a) by A1, A12;

          hence thesis by A13;

        end;

        then ( card nccL) c= ccL by A1, A4, CARD_1: 10;

        then

         A14: nccL c= ccL;

        ccL in nccL by CARD_1: 18;

        hence contradiction by A14, CARD_1: 4;

      end;

      then

      consider O such that

       A15: O in nccL and

       A16: ((f,O) +. a) is_a_fixpoint_of f;

      take O;

      ( card O) in nccL by A15, CARD_1: 9;

      hence ( card O) c= ( card cL) by CARD_3: 91;

      thus thesis by A16;

    end;

    theorem :: KNASTER:31

    

     Th31: for a st (f . a) [= a holds ex O st ( card O) c= ( card the carrier of L) & ((f,O) -. a) is_a_fixpoint_of f

    proof

      let a;

      set cL = the carrier of L;

      set ccL = ( card cL);

      set nccL = ( nextcard ccL);

      deffunc F( Ordinal) = ((f,$1) -. a);

      consider Ls be Sequence such that

       A1: ( dom Ls) = nccL & for O2 be Ordinal st O2 in nccL holds (Ls . O2) = F(O2) from ORDINAL2:sch 2;

      assume

       A2: (f . a) [= a;

      now

        assume

         A3: for O st O in nccL holds not ((f,O) -. a) is_a_fixpoint_of f;

        

         A4: Ls is one-to-one

        proof

          let x1,x2 be object;

          assume that

           A5: x1 in ( dom Ls) and

           A6: x2 in ( dom Ls) and

           A7: (Ls . x1) = (Ls . x2);

          reconsider x1, x2 as Ordinal by A5, A6;

          

           A8: (Ls . x1) = ((f,x1) -. a) by A1, A5;

          

           A9: (Ls . x2) = ((f,x2) -. a) by A1, A6;

          per cases by Lm1;

            suppose

             A10: x1 c< x2;

             not ((f,x2) -. a) is_a_fixpoint_of f by A1, A3, A6;

            hence thesis by A2, A1, A6, A7, A8, A10, Th27;

          end;

            suppose

             A11: x2 c< x1;

             not ((f,x1) -. a) is_a_fixpoint_of f by A1, A3, A5;

            hence thesis by A2, A1, A5, A7, A9, A11, Th27;

          end;

            suppose x2 = x1;

            hence thesis;

          end;

        end;

        ( rng Ls) c= cL

        proof

          let y be object;

          assume y in ( rng Ls);

          then

          consider x be object such that

           A12: x in ( dom Ls) and

           A13: (Ls . x) = y by FUNCT_1:def 3;

          reconsider x as Ordinal by A12;

          (Ls . x) = ((f,x) -. a) by A1, A12;

          hence thesis by A13;

        end;

        then ( card nccL) c= ccL by A1, A4, CARD_1: 10;

        then

         A14: nccL c= ccL;

        ccL in nccL by CARD_1: 18;

        hence contradiction by A14, CARD_1: 4;

      end;

      then

      consider O such that

       A15: O in nccL and

       A16: ((f,O) -. a) is_a_fixpoint_of f;

      take O;

      ( card O) in nccL by A15, CARD_1: 9;

      hence ( card O) c= ( card cL) by CARD_3: 91;

      thus thesis by A16;

    end;

    theorem :: KNASTER:32

    

     Th32: for a, b st a is_a_fixpoint_of f & b is_a_fixpoint_of f holds ex O st ( card O) c= ( card the carrier of L) & ((f,O) +. (a "\/" b)) is_a_fixpoint_of f & a [= ((f,O) +. (a "\/" b)) & b [= ((f,O) +. (a "\/" b))

    proof

      let a, b;

      reconsider ab = (a "\/" b) as Element of L;

      

       A1: a [= ab by LATTICES: 5;

      then

       A2: (f . a) [= (f . ab) by QUANTAL1:def 12;

      

       A3: b [= ab by LATTICES: 5;

      then

       A4: (f . b) [= (f . ab) by QUANTAL1:def 12;

      assume a is_a_fixpoint_of f & b is_a_fixpoint_of f;

      then

       A5: a = (f . a) & b = (f . b);

      then

      consider O such that

       A6: ( card O) c= ( card the carrier of L) & ((f,O) +. ab) is_a_fixpoint_of f by A2, A4, Th30, FILTER_0: 6;

      take O;

      thus ( card O) c= ( card the carrier of L) & ((f,O) +. (a "\/" b)) is_a_fixpoint_of f by A6;

      ab [= (f . ab) by A5, A2, A4, FILTER_0: 6;

      then

       A7: ab [= ((f,O) +. (a "\/" b)) by Th22;

      hence a [= ((f,O) +. (a "\/" b)) by A1, LATTICES: 7;

      thus thesis by A3, A7, LATTICES: 7;

    end;

    theorem :: KNASTER:33

    

     Th33: for a, b st a is_a_fixpoint_of f & b is_a_fixpoint_of f holds ex O st ( card O) c= ( card the carrier of L) & ((f,O) -. (a "/\" b)) is_a_fixpoint_of f & ((f,O) -. (a "/\" b)) [= a & ((f,O) -. (a "/\" b)) [= b

    proof

      let a, b;

      reconsider ab = (a "/\" b) as Element of L;

      

       A1: ab [= a by LATTICES: 6;

      then

       A2: (f . ab) [= (f . a) by QUANTAL1:def 12;

      

       A3: ab [= b by LATTICES: 6;

      then

       A4: (f . ab) [= (f . b) by QUANTAL1:def 12;

      assume a is_a_fixpoint_of f & b is_a_fixpoint_of f;

      then

       A5: a = (f . a) & b = (f . b);

      then

      consider O such that

       A6: ( card O) c= ( card the carrier of L) & ((f,O) -. ab) is_a_fixpoint_of f by A2, A4, Th31, FILTER_0: 7;

      take O;

      thus ( card O) c= ( card the carrier of L) & ((f,O) -. (a "/\" b)) is_a_fixpoint_of f by A6;

      (f . ab) [= ab by A5, A2, A4, FILTER_0: 7;

      then

       A7: ((f,O) -. (a "/\" b)) [= ab by Th23;

      hence ((f,O) -. (a "/\" b)) [= a by A1, LATTICES: 7;

      thus thesis by A3, A7, LATTICES: 7;

    end;

    theorem :: KNASTER:34

    

     Th34: a [= b & b is_a_fixpoint_of f implies for O2 holds ((f,O2) +. a) [= b

    proof

      assume that

       A1: a [= b and

       A2: b is_a_fixpoint_of f;

      defpred S[ Ordinal] means ((f,$1) +. a) [= b;

      

       A3: (f . b) = b by A2;

       A4:

      now

        let O1;

        assume S[O1];

        then (f . ((f,O1) +. a)) [= (f . b) by QUANTAL1:def 12;

        hence S[( succ O1)] by A3, Th15;

      end;

       A5:

      now

        deffunc F( Ordinal) = ((f,$1) +. a);

        let O1;

        assume that

         A6: O1 <> 0 & O1 is limit_ordinal and

         A7: for O2 st O2 in O1 holds S[O2];

        consider L1 be Sequence such that

         A8: ( dom L1) = O1 & for O3 st O3 in O1 holds (L1 . O3) = F(O3) from ORDINAL2:sch 2;

        

         A9: ( rng L1) is_less_than b

        proof

          let q be Element of L;

          assume q in ( rng L1);

          then

          consider O3 be object such that

           A10: O3 in ( dom L1) and

           A11: q = (L1 . O3) by FUNCT_1:def 3;

          reconsider O3 as Ordinal by A10;

          ((f,O3) +. a) [= b by A7, A8, A10;

          hence q [= b by A8, A10, A11;

        end;

        ((f,O1) +. a) = ( "\/" (( rng L1),L)) by A6, A8, Th17;

        hence S[O1] by A9, LATTICE3:def 21;

      end;

      

       A12: S[ 0 ] by A1, Th13;

      thus for O2 holds S[O2] from ORDINAL2:sch 1( A12, A4, A5);

    end;

    theorem :: KNASTER:35

    

     Th35: b [= a & b is_a_fixpoint_of f implies for O2 holds b [= ((f,O2) -. a)

    proof

      assume that

       A1: b [= a and

       A2: b is_a_fixpoint_of f;

      defpred S[ Ordinal] means b [= ((f,$1) -. a);

      

       A3: (f . b) = b by A2;

       A4:

      now

        let O1;

        assume S[O1];

        then (f . b) [= (f . ((f,O1) -. a)) by QUANTAL1:def 12;

        hence S[( succ O1)] by A3, Th16;

      end;

       A5:

      now

        deffunc F( Ordinal) = ((f,$1) -. a);

        let O1;

        assume that

         A6: O1 <> 0 & O1 is limit_ordinal and

         A7: for O2 st O2 in O1 holds S[O2];

        consider L1 be Sequence such that

         A8: ( dom L1) = O1 & for O3 st O3 in O1 holds (L1 . O3) = F(O3) from ORDINAL2:sch 2;

        

         A9: b is_less_than ( rng L1)

        proof

          let q be Element of L;

          assume q in ( rng L1);

          then

          consider O3 be object such that

           A10: O3 in ( dom L1) and

           A11: q = (L1 . O3) by FUNCT_1:def 3;

          reconsider O3 as Ordinal by A10;

          b [= ((f,O3) -. a) by A7, A8, A10;

          hence b [= q by A8, A10, A11;

        end;

        ((f,O1) -. a) = ( "/\" (( rng L1),L)) by A6, A8, Th18;

        hence S[O1] by A9, LATTICE3: 39;

      end;

      

       A12: S[ 0 ] by A1, Th14;

      thus for O2 holds S[O2] from ORDINAL2:sch 1( A12, A4, A5);

    end;

    definition

      let L be complete Lattice, f be UnOp of L;

      :: KNASTER:def9

      func FixPoints f -> strict Lattice means

      : Def9: ex P be non empty with_suprema with_infima Subset of L st P = { x where x be Element of L : x is_a_fixpoint_of f } & it = ( latt P);

      existence

      proof

        defpred P[ set] means $1 is_a_fixpoint_of f;

        set P = { x where x be Element of L : P[x] };

        

         A2: P is Subset of L from DOMAIN_1:sch 7;

        consider a be Element of L such that

         A3: a is_a_fixpoint_of f by A1, Th21;

        

         A4: a in P by A3;

        reconsider P as Subset of L by A2;

        

         A5: P is with_suprema

        proof

          let x,y be Element of L;

          assume that

           A6: x in P and

           A7: y in P;

          consider a be Element of L such that

           A8: x = a and

           A9: a is_a_fixpoint_of f by A6;

          consider b be Element of L such that

           A10: y = b and

           A11: b is_a_fixpoint_of f by A7;

          reconsider a, b as Element of L;

          reconsider ab = (a "\/" b) as Element of L;

          consider O such that ( card O) c= ( card the carrier of L) and

           A12: ((f,O) +. ab) is_a_fixpoint_of f and

           A13: a [= ((f,O) +. ab) & b [= ((f,O) +. ab) by A1, A9, A11, Th32;

          set z = ((f,O) +. ab);

          take z;

          thus z in P by A12;

          thus x [= z & y [= z by A8, A10, A13;

          let z9 be Element of L;

          assume that

           A14: z9 in P and

           A15: x [= z9 & y [= z9;

          

           A16: ex zz be Element of L st zz = z9 & zz is_a_fixpoint_of f by A14;

          ab [= z9 by A8, A10, A15, FILTER_0: 6;

          hence z [= z9 by A1, A16, Th34;

        end;

        P is with_infima

        proof

          let x,y be Element of L;

          assume that

           A17: x in P and

           A18: y in P;

          consider a be Element of L such that

           A19: x = a and

           A20: a is_a_fixpoint_of f by A17;

          consider b be Element of L such that

           A21: y = b and

           A22: b is_a_fixpoint_of f by A18;

          reconsider a, b as Element of L;

          reconsider ab = (a "/\" b) as Element of L;

          consider O such that ( card O) c= ( card the carrier of L) and

           A23: ((f,O) -. ab) is_a_fixpoint_of f and

           A24: ((f,O) -. ab) [= a & ((f,O) -. ab) [= b by A1, A20, A22, Th33;

          set z = ((f,O) -. ab);

          take z;

          thus z in P by A23;

          thus z [= x & z [= y by A19, A21, A24;

          let z9 be Element of L;

          assume that

           A25: z9 in P and

           A26: z9 [= x & z9 [= y;

          

           A27: ex zz be Element of L st zz = z9 & zz is_a_fixpoint_of f by A25;

          z9 [= ab by A19, A21, A26, FILTER_0: 7;

          hence z9 [= z by A1, A27, Th35;

        end;

        then

        reconsider P as non empty with_suprema with_infima Subset of L by A4, A5;

        take ( latt P), P;

        thus P = { x where x be Element of L : x is_a_fixpoint_of f };

        thus thesis;

      end;

      uniqueness ;

    end

    theorem :: KNASTER:36

    

     Th36: the carrier of ( FixPoints f) = { x where x be Element of L : x is_a_fixpoint_of f }

    proof

      ex P be non empty with_suprema with_infima Subset of L st P = { x where x be Element of L : x is_a_fixpoint_of f } & ( FixPoints f) = ( latt P) by Def9;

      hence thesis by Def8;

    end;

    theorem :: KNASTER:37

    

     Th37: the carrier of ( FixPoints f) c= the carrier of L

    proof

      

       A1: the carrier of ( FixPoints f) = { x where x be Element of L : x is_a_fixpoint_of f } by Th36;

      let x be object;

      assume x in the carrier of ( FixPoints f);

      then ex a st x = a & a is_a_fixpoint_of f by A1;

      hence thesis;

    end;

    theorem :: KNASTER:38

    

     Th38: a in the carrier of ( FixPoints f) iff a is_a_fixpoint_of f

    proof

      

       A1: the carrier of ( FixPoints f) = { x where x be Element of L : x is_a_fixpoint_of f } by Th36;

      hereby

        assume a in the carrier of ( FixPoints f);

        then ex b st a = b & b is_a_fixpoint_of f by A1;

        hence a is_a_fixpoint_of f;

      end;

      assume a is_a_fixpoint_of f;

      hence thesis by A1;

    end;

    theorem :: KNASTER:39

    

     Th39: for x,y be Element of ( FixPoints f), a, b st x = a & y = b holds (x [= y iff a [= b)

    proof

      

       A1: ex P be non empty with_suprema with_infima Subset of L st P = { x where x be Element of L : x is_a_fixpoint_of f } & ( FixPoints f) = ( latt P) by Def9;

      let x,y be Element of ( FixPoints f), a, b;

      assume

       A2: x = a & y = b;

      ex a9,b9 be Element of L st x = a9 & y = b9 & (x [= y iff a9 [= b9) by A1, Def8;

      hence thesis by A2;

    end;

    theorem :: KNASTER:40

    ( FixPoints f) is complete

    proof

      set F = ( FixPoints f);

      set cF = the carrier of F;

      set cL = the carrier of L;

      let X be set;

      set Y = (X /\ cF);

      set s = ( "\/" (Y,L));

      

       A1: Y c= cF by XBOOLE_1: 17;

      Y is_less_than (f . s)

      proof

        let q be Element of cL;

        reconsider q9 = q as Element of L;

        assume

         A2: q in Y;

        then q [= s by LATTICE3: 38;

        then

         A3: (f . q) [= (f . s) by QUANTAL1:def 12;

        q9 is_a_fixpoint_of f by A1, A2, Th38;

        hence q [= (f . s) by A3;

      end;

      then

       A4: s [= (f . s) by LATTICE3:def 21;

      then

      consider O such that ( card O) c= ( card cL) and

       A5: ((f,O) +. s) is_a_fixpoint_of f by Th30;

      reconsider p9 = ((f,O) +. s) as Element of L;

      reconsider p = p9 as Element of cF by A5, Th38;

      take p;

      thus X is_less_than p

      proof

        let q be Element of cF;

        q in cF & cF c= cL by Th37;

        then

        reconsider qL9 = q as Element of L;

        assume q in X;

        then q in Y by XBOOLE_0:def 4;

        then

         A6: qL9 [= s by LATTICE3: 38;

        s [= p9 by A4, Th22;

        then qL9 [= p9 by A6, LATTICES: 7;

        hence q [= p by Th39;

      end;

      let r be Element of cF such that

       A7: X is_less_than r;

      reconsider r99 = r as Element of F;

      cF = { x where x be Element of L : x is_a_fixpoint_of f } & r in the carrier of F by Th36;

      then

      consider r9 be Element of L such that

       A8: r9 = r and

       A9: r9 is_a_fixpoint_of f;

      

       A10: Y c= X by XBOOLE_1: 17;

      Y is_less_than r9

      proof

        let q be Element of cL;

        assume

         A11: q in Y;

        then

        reconsider q99 = q as Element of F by A1;

        q99 [= r99 by A10, A7, A11;

        hence q [= r9 by A8, Th39;

      end;

      then s [= r9 by LATTICE3:def 21;

      then p9 [= r9 by A9, Th34;

      hence p [= r by A8, Th39;

    end;

    definition

      let L, f;

      :: KNASTER:def10

      func lfp f -> Element of L equals ((f,( nextcard the carrier of L)) +. ( Bottom L));

      coherence ;

      :: KNASTER:def11

      func gfp f -> Element of L equals ((f,( nextcard the carrier of L)) -. ( Top L));

      coherence ;

    end

    theorem :: KNASTER:41

    

     Th41: ( lfp f) is_a_fixpoint_of f & ex O st ( card O) c= ( card the carrier of L) & ((f,O) +. ( Bottom L)) = ( lfp f)

    proof

      reconsider ze = ( Bottom L) as Element of L;

      

       A1: ( Bottom L) [= (f . ze) by LATTICES: 16;

      then

      consider O such that

       A2: ( card O) c= ( card the carrier of L) and

       A3: ((f,O) +. ( Bottom L)) is_a_fixpoint_of f by Th30;

      ( card the carrier of L) in ( nextcard the carrier of L) by CARD_1:def 3;

      then ( card O) in ( nextcard the carrier of L) by A2, ORDINAL1: 12;

      then O in ( nextcard the carrier of L) by CARD_3: 44;

      then

       A4: O c= ( nextcard the carrier of L) by ORDINAL1:def 2;

      hence ( lfp f) is_a_fixpoint_of f by A1, A3, Th28;

      take O;

      thus ( card O) c= ( card the carrier of L) by A2;

      thus thesis by A1, A3, A4, Th28;

    end;

    theorem :: KNASTER:42

    

     Th42: ( gfp f) is_a_fixpoint_of f & ex O st ( card O) c= ( card the carrier of L) & ((f,O) -. ( Top L)) = ( gfp f)

    proof

      reconsider je = ( Top L) as Element of L;

      

       A1: (f . je) [= ( Top L) by LATTICES: 19;

      then

      consider O such that

       A2: ( card O) c= ( card the carrier of L) and

       A3: ((f,O) -. ( Top L)) is_a_fixpoint_of f by Th31;

      ( card the carrier of L) in ( nextcard the carrier of L) by CARD_1:def 3;

      then ( card O) in ( nextcard the carrier of L) by A2, ORDINAL1: 12;

      then O in ( nextcard the carrier of L) by CARD_3: 44;

      then

       A4: O c= ( nextcard the carrier of L) by ORDINAL1:def 2;

      hence ( gfp f) is_a_fixpoint_of f by A1, A3, Th29;

      take O;

      thus ( card O) c= ( card the carrier of L) by A2;

      thus thesis by A1, A3, A4, Th29;

    end;

    theorem :: KNASTER:43

    

     Th43: a is_a_fixpoint_of f implies ( lfp f) [= a & a [= ( gfp f)

    proof

      defpred S[ Ordinal] means ((f,$1) +. ( Bottom L)) [= a;

       A1:

      now

        deffunc F( Ordinal) = ((f,$1) +. ( Bottom L));

        let O1;

        assume that

         A2: O1 <> 0 & O1 is limit_ordinal and

         A3: for O2 st O2 in O1 holds S[O2];

        consider L1 be Sequence such that

         A4: ( dom L1) = O1 & for O3 st O3 in O1 holds (L1 . O3) = F(O3) from ORDINAL2:sch 2;

        

         A5: ( rng L1) is_less_than a

        proof

          let q be Element of L;

          assume q in ( rng L1);

          then

          consider C be object such that

           A6: C in ( dom L1) and

           A7: q = (L1 . C) by FUNCT_1:def 3;

          reconsider C as Ordinal by A6;

          ((f,C) +. ( Bottom L)) [= a by A3, A4, A6;

          hence q [= a by A4, A6, A7;

        end;

        ((f,O1) +. ( Bottom L)) = ( "\/" (( rng L1),L)) by A2, A4, Th17;

        hence S[O1] by A5, LATTICE3:def 21;

      end;

      assume a is_a_fixpoint_of f;

      then

       A8: (f . a) = a;

       A9:

      now

        let O1;

        assume S[O1];

        then (f . ((f,O1) +. ( Bottom L))) [= (f . a) by QUANTAL1:def 12;

        hence S[( succ O1)] by A8, Th15;

      end;

      ((f, {} ) +. ( Bottom L)) = ( Bottom L) by Th13;

      then

       A10: S[ 0 ] by LATTICES: 16;

      for O2 holds S[O2] from ORDINAL2:sch 1( A10, A9, A1);

      hence ( lfp f) [= a;

      defpred S[ Ordinal] means a [= ((f,$1) -. ( Top L));

       A11:

      now

        let O1;

        assume S[O1];

        then (f . a) [= (f . ((f,O1) -. ( Top L))) by QUANTAL1:def 12;

        hence S[( succ O1)] by A8, Th16;

      end;

       A12:

      now

        deffunc F( Ordinal) = ((f,$1) -. ( Top L));

        let O1;

        assume that

         A13: O1 <> 0 & O1 is limit_ordinal and

         A14: for O2 st O2 in O1 holds S[O2];

        consider L1 be Sequence such that

         A15: ( dom L1) = O1 & for O3 st O3 in O1 holds (L1 . O3) = F(O3) from ORDINAL2:sch 2;

        

         A16: a is_less_than ( rng L1)

        proof

          let q be Element of L;

          assume q in ( rng L1);

          then

          consider C be object such that

           A17: C in ( dom L1) and

           A18: q = (L1 . C) by FUNCT_1:def 3;

          reconsider C as Ordinal by A17;

          a [= ((f,C) -. ( Top L)) by A14, A15, A17;

          hence a [= q by A15, A17, A18;

        end;

        ((f,O1) -. ( Top L)) = ( "/\" (( rng L1),L)) by A13, A15, Th18;

        hence S[O1] by A16, LATTICE3: 39;

      end;

      ((f, {} ) -. ( Top L)) = ( Top L) by Th14;

      then

       A19: S[ 0 ] by LATTICES: 19;

      for O2 holds S[O2] from ORDINAL2:sch 1( A19, A11, A12);

      hence thesis;

    end;

    theorem :: KNASTER:44

    (f . a) [= a implies ( lfp f) [= a

    proof

      assume

       A1: (f . a) [= a;

      then

      consider O such that ( card O) c= ( card the carrier of L) and

       A2: ((f,O) -. a) is_a_fixpoint_of f by Th31;

      

       A3: ( lfp f) [= ((f,O) -. a) by A2, Th43;

      ((f,O) -. a) [= a by A1, Th23;

      hence thesis by A3, LATTICES: 7;

    end;

    theorem :: KNASTER:45

    a [= (f . a) implies a [= ( gfp f)

    proof

      assume

       A1: a [= (f . a);

      then

      consider O such that ( card O) c= ( card the carrier of L) and

       A2: ((f,O) +. a) is_a_fixpoint_of f by Th30;

      

       A3: ((f,O) +. a) [= ( gfp f) by A2, Th43;

      a [= ((f,O) +. a) by A1, Th22;

      hence thesis by A3, LATTICES: 7;

    end;

    begin

    reserve f for monotone UnOp of ( BooleLatt A);

    theorem :: KNASTER:46

    

     Th46: for f be UnOp of ( BooleLatt A) holds f is monotone iff f is c=-monotone

    proof

      let f be UnOp of ( BooleLatt A);

      thus f is monotone implies f is c=-monotone

      proof

        assume

         A1: f is monotone;

        let x,y be Element of ( BooleLatt A);

        assume x c= y;

        then x [= y by LATTICE3: 2;

        then (f . x) [= (f . y) by A1;

        hence thesis by LATTICE3: 2;

      end;

      assume

       A2: f is c=-monotone;

      let p,q be Element of ( BooleLatt A);

      assume p [= q;

      then p c= q by LATTICE3: 2;

      then (f . p) c= (f . q) by A2;

      hence (f . p) [= (f . q) by LATTICE3: 2;

    end;

    theorem :: KNASTER:47

    ex g be c=-monotone Function of ( bool A), ( bool A) st ( lfp (A,g)) = ( lfp f)

    proof

      reconsider lf = ( lfp f) as Subset of A by LATTICE3:def 1;

      the carrier of ( BooleLatt A) = ( bool A) by LATTICE3:def 1;

      then

      reconsider g = f as c=-monotone Function of ( bool A), ( bool A) by Th46;

      reconsider lg = ( lfp (A,g)) as Element of ( BooleLatt A) by LATTICE3:def 1;

      take g;

      lg is_a_fixpoint_of f by Th4;

      then ( lfp f) [= lg by Th43;

      then

       A1: lf c= lg by LATTICE3: 2;

      ( lfp f) is_a_fixpoint_of f by Th41;

      then ( lfp (A,g)) c= lf by Th8;

      hence thesis by A1;

    end;

    theorem :: KNASTER:48

    ex g be c=-monotone Function of ( bool A), ( bool A) st ( gfp (A,g)) = ( gfp f)

    proof

      reconsider gf = ( gfp f) as Subset of A by LATTICE3:def 1;

      the carrier of ( BooleLatt A) = ( bool A) by LATTICE3:def 1;

      then

      reconsider g = f as c=-monotone Function of ( bool A), ( bool A) by Th46;

      reconsider gg = ( gfp (A,g)) as Element of ( BooleLatt A) by LATTICE3:def 1;

      take g;

      gg is_a_fixpoint_of f by Th5;

      then gg [= ( gfp f) by Th43;

      then

       A1: gg c= gf by LATTICE3: 2;

      ( gfp f) is_a_fixpoint_of f by Th42;

      then gf c= ( gfp (A,g)) by Th8;

      hence thesis by A1;

    end;