:: KNASTER semantic presentation

begin


theorem :: KNASTER:1
for h, f, g being Function st h = f \/ g & dom f misses dom g holds
( h is one-to-one iff ( f is one-to-one & g is one-to-one & rng f misses rng g ) )
proof
let h, f, g be Function; ::_thesis: ( 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 ) ) )
assume that
A1: h = f \/ g and
A2: dom f misses dom g ; ::_thesis: ( h is one-to-one iff ( f is one-to-one & g is one-to-one & rng f misses rng g ) )
A3: dom h = (dom f) \/ (dom g) by A1, RELAT_1:1;
hereby  ::_thesis: ( f is one-to-one & g is one-to-one & rng f misses rng g implies h is one-to-one )
assume A4: h is one-to-one ; ::_thesis: ( f is one-to-one & g is one-to-one & rng f misses rng g )
thus  f is one-to-one ::_thesis: ( g is one-to-one & rng f misses rng g )
proof
assume  not f is one-to-one ; ::_thesis: contradiction
then consider x1, x2 being set  such that
A5: x1 in dom f and
A6: x2 in dom f and
A7: ( f . x1 = f . x2 & x1 <> x2 ) by FUNCT_1:def_4;
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, FUNCT_1:def_4; ::_thesis: verum
end;
thus  g is one-to-one ::_thesis: rng f misses rng g
proof
assume  not g is one-to-one ; ::_thesis: contradiction
then consider x1, x2 being set  such that
A11: x1 in dom g and
A12: x2 in dom g and
A13: ( g . x1 = g . x2 & x1 <> x2 ) by FUNCT_1:def_4;
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, FUNCT_1:def_4; ::_thesis: verum
end;
thus  rng f misses rng g ::_thesis: verum
proof
assume  not rng f misses rng g ; ::_thesis: contradiction
then consider hx being set  such that
A17: hx in rng f and
A18: hx in rng g by XBOOLE_0:3;
consider x1 being set  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 being set  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;
 [x2,hx] in g by A22, A23, FUNCT_1:def_2;
then  [x2,hx] in h by A1, XBOOLE_0:def_3;
then A25: h . x2 = hx by A24, FUNCT_1:def_2;
A26: 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;
hence  contradiction by A4, A26, A21, A24, A25, FUNCT_1:def_4; ::_thesis: verum
end;
end;
assume A27: ( f is one-to-one & g is one-to-one & rng f misses rng g ) ; ::_thesis: h is one-to-one
 f \/ g = f +* g by A2, FUNCT_4:31;
hence  h is one-to-one by A1, A27, FUNCT_4:92; ::_thesis: verum
end;

begin


theorem Th2: :: KNASTER:2
for X, x being set
for n being Element of NAT
for f being Function of X,X st x is_a_fixpoint_of iter (f,n) holds
f . x is_a_fixpoint_of iter (f,n)
proof
let X, x be set ; ::_thesis: for n being Element of NAT
for f being Function of X,X st x is_a_fixpoint_of iter (f,n) holds
f . x is_a_fixpoint_of iter (f,n)
let n be Element of NAT ; ::_thesis: for f being Function of X,X st x is_a_fixpoint_of iter (f,n) holds
f . x is_a_fixpoint_of iter (f,n)
let f be Function of X,X; ::_thesis: ( x is_a_fixpoint_of iter (f,n) implies f . x is_a_fixpoint_of iter (f,n) )
assume A1: x is_a_fixpoint_of iter (f,n) ; ::_thesis: f . x is_a_fixpoint_of iter (f,n)
then A2: x in dom (iter (f,n)) by ABIAN:def_3;
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)) ; :: according to ABIAN:def_3 ::_thesis: f . x = (iter (f,n)) . (f . x)
 x = (iter (f,n)) . x by A1, ABIAN:def_3;
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 ;
::_thesis: verum
end;

theorem :: KNASTER:3
for X, x being set
for f being Function of X,X st ex n being Element of NAT st
( x is_a_fixpoint_of iter (f,n) & ( for y being set st y is_a_fixpoint_of iter (f,n) holds
x = y ) ) holds
x is_a_fixpoint_of f
proof
let X, x be set ; ::_thesis: for f being Function of X,X st ex n being Element of NAT st
( x is_a_fixpoint_of iter (f,n) & ( for y being set st y is_a_fixpoint_of iter (f,n) holds
x = y ) ) holds
x is_a_fixpoint_of f
let f be Function of X,X; ::_thesis: ( ex n being Element of NAT st
( x is_a_fixpoint_of iter (f,n) & ( for y being set st y is_a_fixpoint_of iter (f,n) holds
x = y ) ) implies x is_a_fixpoint_of f )
given n being Element of NAT  such that A1: x is_a_fixpoint_of iter (f,n) and
A2: for y being set st y is_a_fixpoint_of iter (f,n) holds
x = y ; ::_thesis: x is_a_fixpoint_of f
 ( dom f = X & dom (iter (f,n)) = X ) by FUNCT_2:52;
hence  x in dom f by A1, ABIAN:def_3; :: according to ABIAN:def_3 ::_thesis: x = f . x
thus  x = f . x by A1, A2, Th2; ::_thesis: verum
end;

definition
let A, B be non empty set ;
let f be Function of A,B;
:: original: c=-monotone
redefine attrf is c=-monotone  means :Def1: :: KNASTER:def 1
 for x, y being Element of A st x c= y holds
f . x c= f . y;
compatibility
 ( f is c=-monotone iff for x, y being Element of A st x c= y holds
f . x c= f . y )
proof
 dom f = A by FUNCT_2:def_1;
hence  ( f is c=-monotone implies for x, y being Element of A st x c= y holds
f . x c= f . y ) by COHSP_1:def_11; ::_thesis: ( ( for x, y being Element of A st x c= y holds
f . x c= f . y ) implies f is c=-monotone )
assume A1: for x, y being Element of A st x c= y holds
f . x c= f . y ; ::_thesis: f is c=-monotone
let x, y be set ; :: according to COHSP_1:def_11 ::_thesis: ( not x in dom f or not y in dom f or not x c= y or f . x c= f . y )
assume  ( x in dom f & y in dom f & x c= y ) ; ::_thesis: f . x c= f . y
hence  f . x c= f . y by A1; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines c=-monotone KNASTER:def_1_:_
 for A, B being non empty set
for f being Function of A,B holds
( f is c=-monotone iff for x, y being Element of A st x c= y holds
f . x c= f . y );

registration
let A be set ;
let B be non empty set ;
cluster Relation-like A -defined B -valued Function-like quasi_total c=-monotone for Element of bool [:A,B:];
existence
 ex b1 being Function of A,B st b1 is c=-monotone
proof
set b = the Element of B;
reconsider f = A --> the Element of B as Function of A,B ;
take  f ; ::_thesis: f is c=-monotone
let x, y be set ; :: according to COHSP_1:def_11 ::_thesis: ( not x in dom f or not y in dom f or not x c= y or f . x c= f . y )
assume that
A1: x in dom f and
A2: y in dom f and
 x c= y ; ::_thesis: f . x c= f . y
f . x = the Element of B by A1, FUNCOP_1:7
.= f . y by A2, FUNCOP_1:7 ;
hence  f . x c= f . y ; ::_thesis: verum
end;
end;

definition
let X be set ;
let f be V220() Function of (bool X),(bool X);
func lfp (X,f) ->  Subset of X equals :: KNASTER:def 2
 meet  {  h where h is Subset of X : f . h c= h  }  ;
coherence
 meet  {  h where h is Subset of X : f . h c= h  }  is Subset of X
proof
defpred S1[ set ] means f . $1 c= $1;
reconsider H =  {  h where h is Subset of X : S1[h]  }  as Subset-Family of X from DOMAIN_1:sch_7();
reconsider H = H as Subset-Family of X ;
 meet H is Subset of X ;
hence  meet  {  h where h is Subset of X : f . h c= h  }  is Subset of X ; ::_thesis: verum
end;
func gfp (X,f) ->  Subset of X equals :: KNASTER:def 3
 union  {  h where h is Subset of X : h c= f . h  }  ;
coherence
 union  {  h where h is Subset of X : h c= f . h  }  is Subset of X
proof
defpred S1[ set ] means $1 c= f . $1;
reconsider H =  {  h where h is Subset of X : S1[h]  }  as Subset-Family of X from DOMAIN_1:sch_7();
 union H is Subset of X ;
hence  union  {  h where h is Subset of X : h c= f . h  }  is Subset of X ; ::_thesis: verum
end;
end;

:: deftheorem  defines lfp KNASTER:def_2_:_
 for X being set
for f being V220() Function of (bool X),(bool X) holds lfp (X,f) = meet  {  h where h is Subset of X : f . h c= h  }  ;

:: deftheorem  defines gfp KNASTER:def_3_:_
 for X being set
for f being V220() Function of (bool X),(bool X) holds gfp (X,f) = union  {  h where h is Subset of X : h c= f . h  }  ;


theorem Th4: :: KNASTER:4
for X being set
for f being V220() Function of (bool X),(bool X) holds lfp (X,f) is_a_fixpoint_of f
proof
let X be set ; ::_thesis: for f being V220() Function of (bool X),(bool X) holds lfp (X,f) is_a_fixpoint_of f
let f be V220() Function of (bool X),(bool X); ::_thesis: lfp (X,f) is_a_fixpoint_of f
defpred S1[ set ] means f . $1 c= $1;
reconsider H =  {  h where h is Subset of X : S1[h]  }  as Subset-Family of X from DOMAIN_1:sch_7();
reconsider H = H as Subset-Family of X ;
set A = meet H;
now__::_thesis:_(_H_<>_{}_&_(_for_h_being_set_st_h_in_H_holds_
f_._(meet_H)_c=_h_)_)
 X c= X ;
then reconsider X9 = X as Subset of X ;
 f . X9 c= X9 ;
then  X9 in H ;
hence  H <> {} ; ::_thesis: for h being set st h in H holds
f . (meet H) c= h
let h be set ; ::_thesis: ( h in H implies f . (meet H) c= h )
assume A1: h in H ; ::_thesis: f . (meet H) c= h
then consider x being Subset of X such that
A2: x = h and
A3: f . x c= x ;
 meet H c= h by A1, SETFAM_1:3;
then  f . (meet H) c= f . x by A2, Def1;
hence  f . (meet H) c= h by A2, A3, XBOOLE_1:1; ::_thesis: verum
end;
then A4: f . (meet H) c= meet H by SETFAM_1:5;
then  f . (f . (meet H)) c= f . (meet H) by Def1;
then  f . (meet H) in H ;
then  meet H c= f . (meet H) by SETFAM_1:3;
hence  f . (lfp (X,f)) = lfp (X,f) by A4, XBOOLE_0:def_10; :: according to ABIAN:def_4 ::_thesis: verum
end;

theorem Th5: :: KNASTER:5
for X being set
for f being V220() Function of (bool X),(bool X) holds gfp (X,f) is_a_fixpoint_of f
proof
let X be set ; ::_thesis: for f being V220() Function of (bool X),(bool X) holds gfp (X,f) is_a_fixpoint_of f
let f be V220() Function of (bool X),(bool X); ::_thesis: gfp (X,f) is_a_fixpoint_of f
defpred S1[ set ] means $1 c= f . $1;
reconsider H =  {  h where h is Subset of X : S1[h]  }  as Subset-Family of X from DOMAIN_1:sch_7();
set A = union H;
now__::_thesis:_for_x_being_set_st_x_in_H_holds_
x_c=_f_._(union_H)
let x be set ; ::_thesis: ( x in H implies x c= f . (union H) )
assume A1: x in H ; ::_thesis: x c= f . (union H)
then consider h being Subset of X such that
A2: x = h and
A3: h c= f . h ;
 h c= union H by A1, A2, ZFMISC_1:74;
then  f . h c= f . (union H) by Def1;
hence  x c= f . (union H) by A2, A3, XBOOLE_1:1; ::_thesis: verum
end;
then A4: union H c= f . (union H) by ZFMISC_1:76;
then  f . (union H) c= f . (f . (union H)) by Def1;
then  f . (union H) in H ;
then  f . (union H) c= union H by ZFMISC_1:74;
hence  f . (gfp (X,f)) = gfp (X,f) by A4, XBOOLE_0:def_10; :: according to ABIAN:def_4 ::_thesis: verum
end;

theorem Th6: :: KNASTER:6
for X being set
for f being V220() Function of (bool X),(bool X)
for S being Subset of X st f . S c= S holds
lfp (X,f) c= S
proof
let X be set ; ::_thesis: for f being V220() Function of (bool X),(bool X)
for S being Subset of X st f . S c= S holds
lfp (X,f) c= S
let f be V220() Function of (bool X),(bool X); ::_thesis: for S being Subset of X st f . S c= S holds
lfp (X,f) c= S
let S be Subset of X; ::_thesis: ( f . S c= S implies lfp (X,f) c= S )
set H =  {  h where h is Subset of X : f . h c= h  }  ;
assume  f . S c= S ; ::_thesis: lfp (X,f) c= S
then  S in  {  h where h is Subset of X : f . h c= h  }  ;
hence  lfp (X,f) c= S by SETFAM_1:3; ::_thesis: verum
end;

theorem Th7: :: KNASTER:7
for X being set
for f being V220() Function of (bool X),(bool X)
for S being Subset of X st S c= f . S holds
S c= gfp (X,f)
proof
let X be set ; ::_thesis: for f being V220() Function of (bool X),(bool X)
for S being Subset of X st S c= f . S holds
S c= gfp (X,f)
let f be V220() Function of (bool X),(bool X); ::_thesis: for S being Subset of X st S c= f . S holds
S c= gfp (X,f)
let S be Subset of X; ::_thesis: ( S c= f . S implies S c= gfp (X,f) )
set H =  {  h where h is Subset of X : h c= f . h  }  ;
assume  S c= f . S ; ::_thesis: S c= gfp (X,f)
then  S in  {  h where h is Subset of X : h c= f . h  }  ;
hence  S c= gfp (X,f) by ZFMISC_1:74; ::_thesis: verum
end;

theorem Th8: :: KNASTER:8
for X being set
for f being V220() Function of (bool X),(bool X)
for S being Subset of X st S is_a_fixpoint_of f holds
( lfp (X,f) c= S & S c= gfp (X,f) )
proof
let X be set ; ::_thesis: for f being V220() Function of (bool X),(bool X)
for S being Subset of X st S is_a_fixpoint_of f holds
( lfp (X,f) c= S & S c= gfp (X,f) )
let f be V220() Function of (bool X),(bool X); ::_thesis: for S being Subset of X st S is_a_fixpoint_of f holds
( lfp (X,f) c= S & S c= gfp (X,f) )
let S be Subset of X; ::_thesis: ( S is_a_fixpoint_of f implies ( lfp (X,f) c= S & S c= gfp (X,f) ) )
assume  S = f . S ; :: according to ABIAN:def_4 ::_thesis: ( lfp (X,f) c= S & S c= gfp (X,f) )
hence  ( lfp (X,f) c= S & S c= gfp (X,f) ) by Th6, Th7; ::_thesis: verum
end;

scheme :: KNASTER:sch 1
Knaster{ F1() ->  set , F2( set ) ->  set } :
 ex D being set st
( F2(D) = D & D c= F1() )
provided
A1: for X, Y being set st X c= Y holds
F2(X) c= F2(Y) and
A2: F2(F1()) c= F1()
proof
consider f being Function such that
A3: ( dom f = bool F1() & ( for x being set st x in bool F1() holds
f . x = F2(x) ) ) from FUNCT_1:sch_3();
 rng f c= bool F1()
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in bool F1() )
assume  x in rng f ; ::_thesis: x in bool F1()
then consider y being set  such that
A4: y in dom f and
A5: x = f . y by FUNCT_1:def_3;
 F2(y) c= F2(F1()) by A1, A3, A4;
then  F2(y) c= F1() by A2, XBOOLE_1:1;
then  f . y c= F1() by A3, A4;
hence  x in bool F1() by A5; ::_thesis: verum
end;
then reconsider f = f as Function of (bool F1()),(bool F1()) by A3, FUNCT_2:def_1, RELSET_1:4;
now__::_thesis:_for_a,_b_being_set_st_a_in_dom_f_&_b_in_dom_f_&_a_c=_b_holds_
f_._a_c=_f_._b
let a, b be set ; ::_thesis: ( a in dom f & b in dom f & a c= b implies f . a c= f . b )
assume that
A6: ( a in dom f & b in dom f ) and
A7: a c= b ; ::_thesis: f . a c= f . b
 ( f . a = F2(a) & f . b = F2(b) ) by A3, A6;
hence  f . a c= f . b by A1, A7; ::_thesis: verum
end;
then reconsider f = f as V220() Function of (bool F1()),(bool F1()) by COHSP_1:def_11;
take d = lfp (F1(),f); ::_thesis: ( F2(d) = d & d c= F1() )
 d is_a_fixpoint_of f by Th4;
then  d = f . d by ABIAN:def_3;
hence  F2(d) = d by A3; ::_thesis: d c= F1()
thus  d c= F1() ; ::_thesis: verum
end;


theorem Th9: :: KNASTER:9
for X, Y being non empty set
for f being Function of X,Y
for g being Function of Y,X ex Xa, Xb, Ya, Yb being set st
( Xa misses Xb & Ya misses Yb & Xa \/ Xb = X & Ya \/ Yb = Y & f .: Xa = Ya & g .: Yb = Xb )
proof
let X, Y be non empty set ; ::_thesis: for f being Function of X,Y
for g being Function of Y,X ex Xa, Xb, Ya, Yb being set st
( Xa misses Xb & Ya misses Yb & Xa \/ Xb = X & Ya \/ Yb = Y & f .: Xa = Ya & g .: Yb = Xb )
let f be Function of X,Y; ::_thesis: for g being Function of Y,X ex Xa, Xb, Ya, Yb being set st
( Xa misses Xb & Ya misses Yb & Xa \/ Xb = X & Ya \/ Yb = Y & f .: Xa = Ya & g .: Yb = Xb )
let g be Function of Y,X; ::_thesis: ex Xa, Xb, Ya, Yb being set st
( Xa misses Xb & Ya misses Yb & Xa \/ Xb = X & Ya \/ Yb = Y & f .: Xa = Ya & g .: Yb = Xb )
deffunc H1( set ) ->  Element of bool X = X \ (g .: (Y \ (f .: $1)));
A1: for x being set st x in bool X holds
H1(x) in bool X ;
consider h being Function of (bool X),(bool X) such that
A2: for x being set st x in bool X holds
h . x = H1(x) from FUNCT_2:sch_2(A1);
now__::_thesis:_for_x,_y_being_set_st_x_in_dom_h_&_y_in_dom_h_&_x_c=_y_holds_
h_._x_c=_h_._y
let x, y be set ; ::_thesis: ( x in dom h & y in dom h & x c= y implies h . x c= h . y )
assume that
A3: x in dom h and
A4: y in dom h and
A5: x c= y ; ::_thesis: h . x c= h . 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; ::_thesis: verum
end;
then reconsider h = h as V220() Function of (bool X),(bool X) by COHSP_1:def_11;
take Xa = lfp (X,h); ::_thesis: ex Xb, Ya, Yb being set st
( Xa misses Xb & Ya misses Yb & Xa \/ Xb = X & Ya \/ Yb = Y & f .: Xa = Ya & g .: Yb = Xb )
take Xb = X \ Xa; ::_thesis: ex Ya, Yb being set st
( Xa misses Xb & Ya misses Yb & Xa \/ Xb = X & Ya \/ Yb = Y & f .: Xa = Ya & g .: Yb = Xb )
take Ya = f .: Xa; ::_thesis: ex Yb being set st
( Xa misses Xb & Ya misses Yb & Xa \/ Xb = X & Ya \/ Yb = Y & f .: Xa = Ya & g .: Yb = Xb )
take Yb = Y \ Ya; ::_thesis: ( Xa misses Xb & Ya misses Yb & Xa \/ Xb = X & Ya \/ Yb = Y & f .: Xa = Ya & g .: Yb = Xb )
thus  Xa misses Xb by XBOOLE_1:79; ::_thesis: ( Ya misses Yb & Xa \/ Xb = X & Ya \/ Yb = Y & f .: Xa = Ya & g .: Yb = Xb )
thus  Ya misses Yb by XBOOLE_1:79; ::_thesis: ( Xa \/ Xb = X & Ya \/ Yb = Y & f .: Xa = Ya & g .: Yb = Xb )
thus  Xa \/ Xb = X by XBOOLE_1:45; ::_thesis: ( Ya \/ Yb = Y & f .: Xa = Ya & g .: Yb = Xb )
thus  Ya \/ Yb = Y by XBOOLE_1:45; ::_thesis: ( f .: Xa = Ya & g .: Yb = Xb )
thus  f .: Xa = Ya ; ::_thesis: g .: Yb = Xb
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, ABIAN:def_3 ; ::_thesis: verum
end;

theorem Th10: :: KNASTER:10
for X, Y being non empty set
for f being Function of X,Y
for g being Function of Y,X st f is one-to-one & g is one-to-one holds
ex h being Function of X,Y st h is bijective
proof
let X, Y be non empty set ; ::_thesis: for f being Function of X,Y
for g being Function of Y,X st f is one-to-one & g is one-to-one holds
ex h being Function of X,Y st h is bijective
let f be Function of X,Y; ::_thesis: for g being Function of Y,X st f is one-to-one & g is one-to-one holds
ex h being Function of X,Y st h is bijective
let g be Function of Y,X; ::_thesis: ( f is one-to-one & g is one-to-one implies ex h being Function of X,Y st h is bijective )
assume that
A1: f is one-to-one and
A2: g is one-to-one ; ::_thesis: ex h being Function of X,Y st h is bijective
consider Xa, Xb, Ya, Yb being 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: g | Yb is one-to-one by A2, FUNCT_1:52;
set fXa = f | Xa;
 dom f = X by FUNCT_2:def_1;
then A10: dom (f | Xa) = Xa by A5, RELAT_1:62, XBOOLE_1:7;
set h = (f | Xa) +* ((g | Yb) ");
 rng (g | Yb) = Xb by A8, RELAT_1:115;
then A11: dom ((g | Yb) ") = Xb by A9, FUNCT_1:32;
then A12: X = dom ((f | Xa) +* ((g | Yb) ")) by A5, A10, FUNCT_4:def_1;
A13: rng (f | Xa) = Ya by A7, RELAT_1:115;
 dom g = Y by FUNCT_2:def_1;
then  dom (g | Yb) = Yb by A6, RELAT_1:62, XBOOLE_1:7;
then A14: rng ((g | Yb) ") = Yb by A9, FUNCT_1:33;
 (f | Xa) \/ ((g | Yb) ") = (f | Xa) +* ((g | Yb) ") by A3, A10, A11, FUNCT_4:31;
then A15: rng ((f | Xa) +* ((g | Yb) ")) = Y by A6, A13, A14, RELAT_1:12;
then reconsider h = (f | Xa) +* ((g | Yb) ") 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 ; ::_thesis: h is bijective
 f | Xa is one-to-one by A1, FUNCT_1:52;
then  h is one-to-one by A4, A13, A9, A14, FUNCT_4:92;
hence  h is bijective by A16, FUNCT_2:def_4; ::_thesis: verum
end;

theorem Th11: :: KNASTER:11
for X, Y being non empty set
for f being Function of X,Y st f is bijective holds
X,Y are_equipotent
proof
let X, Y be non empty set ; ::_thesis: for f being Function of X,Y st f is bijective holds
X,Y are_equipotent
let f be Function of X,Y; ::_thesis: ( f is bijective implies X,Y are_equipotent )
assume A1: f is bijective ; ::_thesis: X,Y are_equipotent
take h = f; :: according to TARSKI:def_6 ::_thesis: ( ( for b1 being set holds
( not b1 in X or ex b2 being set st
( b2 in Y & [b1,b2] in h ) ) ) & ( for b1 being set holds
( not b1 in Y or ex b2 being set st
( b2 in X & [b2,b1] in h ) ) ) & ( for b1, b2, b3, b4 being set holds
( not [b1,b2] in h or not [b3,b4] in h or ( ( not b1 = b3 or b2 = b4 ) & ( not b2 = b4 or b1 = b3 ) ) ) ) )
A2: ( h is one-to-one & h is onto ) by A1, FUNCT_2:def_4;
then A3: rng h = Y by FUNCT_2:def_3;
hereby  ::_thesis: ( ( for b1 being set holds
( not b1 in Y or ex b2 being set st
( b2 in X & [b2,b1] in h ) ) ) & ( for b1, b2, b3, b4 being set holds
( not [b1,b2] in h or not [b3,b4] in h or ( ( not b1 = b3 or b2 = b4 ) & ( not b2 = b4 or b1 = b3 ) ) ) ) )
let x be set ; ::_thesis: ( x in X implies ex y being set st
( y in Y & [x,y] in h ) )
assume A4: x in X ; ::_thesis: ex y being set st
( y in Y & [x,y] in h )
take y = h . x; ::_thesis: ( y in Y & [x,y] in h )
thus  y in Y by A3, A4, FUNCT_2:4; ::_thesis: [x,y] in h
 x in dom h by A4, FUNCT_2:def_1;
hence  [x,y] in h by FUNCT_1:1; ::_thesis: verum
end;
hereby  ::_thesis: for b1, b2, b3, b4 being set holds
( not [b1,b2] in h or not [b3,b4] in h or ( ( not b1 = b3 or b2 = b4 ) & ( not b2 = b4 or b1 = b3 ) ) )
let y be set ; ::_thesis: ( y in Y implies ex x being set st
( x in X & [x,y] in h ) )
assume  y in Y ; ::_thesis: ex x being set st
( x in X & [x,y] in h )
then consider x being set  such that
A5: ( x in dom h & y = h . x ) by A3, FUNCT_1:def_3;
take x = x; ::_thesis: ( x in X & [x,y] in h )
thus  ( x in X & [x,y] in h ) by A5, FUNCT_1:1; ::_thesis: verum
end;
let x, y, z, u be set ; ::_thesis: ( not [x,y] in h or not [z,u] in h or ( ( not x = z or y = u ) & ( not y = u or x = z ) ) )
assume that
A6: [x,y] in h and
A7: [z,u] in h ; ::_thesis: ( ( not x = z or y = u ) & ( not y = u or x = z ) )
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  ( ( not x = z or y = u ) & ( not y = u or x = z ) ) by A2, A8, FUNCT_1:def_4; ::_thesis: verum
end;

theorem :: KNASTER:12
for X, Y being non empty set
for f being Function of X,Y
for g being Function of Y,X st f is one-to-one & g is one-to-one holds
X,Y are_equipotent
proof
let X, Y be non empty set ; ::_thesis: for f being Function of X,Y
for g being Function of Y,X st f is one-to-one & g is one-to-one holds
X,Y are_equipotent
let f be Function of X,Y; ::_thesis: for g being Function of Y,X st f is one-to-one & g is one-to-one holds
X,Y are_equipotent
let g be Function of Y,X; ::_thesis: ( f is one-to-one & g is one-to-one implies X,Y are_equipotent )
assume  ( f is one-to-one & g is one-to-one ) ; ::_thesis: X,Y are_equipotent
then  ex h being Function of X,Y st h is bijective by Th10;
hence  X,Y are_equipotent by Th11; ::_thesis: verum
end;

begin

definition
let L be Lattice;
let f be Function of the carrier of L, the carrier of L;
let x be Element of L;
let O be Ordinal;
func(f,O) +. x ->  set  means :Def4: :: KNASTER:def 4
 ex L0 being T-Sequence st
( it = last L0 & dom L0 = succ O & L0 . {} = x & ( for C being Ordinal st succ C in succ O holds
L0 . (succ C) = f . (L0 . C) ) & ( for C being Ordinal st C in succ O & C <> {} & C is limit_ordinal holds
L0 . C = "\/" ((rng (L0 | C)),L) ) );
correctness
existence
ex b1 being set ex L0 being T-Sequence st
( b1 = last L0 & dom L0 = succ O & L0 . {} = x & ( for C being Ordinal st succ C in succ O holds
L0 . (succ C) = f . (L0 . C) ) & ( for C being Ordinal st C in succ O & C <> {} & C is limit_ordinal holds
L0 . C = "\/" ((rng (L0 | C)),L) ) );
uniqueness
for b1, b2 being set st ex L0 being T-Sequence st
( b1 = last L0 & dom L0 = succ O & L0 . {} = x & ( for C being Ordinal st succ C in succ O holds
L0 . (succ C) = f . (L0 . C) ) & ( for C being Ordinal st C in succ O & C <> {} & C is limit_ordinal holds
L0 . C = "\/" ((rng (L0 | C)),L) ) ) & ex L0 being T-Sequence st
( b2 = last L0 & dom L0 = succ O & L0 . {} = x & ( for C being Ordinal st succ C in succ O holds
L0 . (succ C) = f . (L0 . C) ) & ( for C being Ordinal st C in succ O & C <> {} & C is limit_ordinal holds
L0 . C = "\/" ((rng (L0 | C)),L) ) ) holds
b1 = b2;
proof
deffunc H1( Ordinal, T-Sequence) ->  Element of the carrier of L = "\/" ((rng $2),L);
deffunc H2( Ordinal, set ) ->  set = f . $2;
 ( ex z being set ex S being T-Sequence st
( z = last S & dom S = succ O & S . {} = x & ( for C being Ordinal st succ C in succ O holds
S . (succ C) = H2(C,S . C) ) & ( for C being Ordinal st C in succ O & C <> {} & C is limit_ordinal holds
S . C = H1(C,S | C) ) ) & ( for x1, x2 being set st ex L0 being T-Sequence st
( x1 = last L0 & dom L0 = succ O & L0 . {} = x & ( for C being Ordinal st succ C in succ O holds
L0 . (succ C) = H2(C,L0 . C) ) & ( for C being Ordinal st C in succ O & C <> {} & C is limit_ordinal holds
L0 . C = H1(C,L0 | C) ) ) & ex L0 being T-Sequence st
( x2 = last L0 & dom L0 = succ O & L0 . {} = x & ( for C being Ordinal st succ C in succ O holds
L0 . (succ C) = H2(C,L0 . C) ) & ( for C being Ordinal st C in succ O & C <> {} & C is limit_ordinal holds
L0 . C = H1(C,L0 | C) ) ) holds
x1 = x2 ) ) from ORDINAL2:sch_7();
hence  ( ex b1 being set ex L0 being T-Sequence st
( b1 = last L0 & dom L0 = succ O & L0 . {} = x & ( for C being Ordinal st succ C in succ O holds
L0 . (succ C) = f . (L0 . C) ) & ( for C being Ordinal st C in succ O & C <> {} & C is limit_ordinal holds
L0 . C = "\/" ((rng (L0 | C)),L) ) ) & ( for b1, b2 being set st ex L0 being T-Sequence st
( b1 = last L0 & dom L0 = succ O & L0 . {} = x & ( for C being Ordinal st succ C in succ O holds
L0 . (succ C) = f . (L0 . C) ) & ( for C being Ordinal st C in succ O & C <> {} & C is limit_ordinal holds
L0 . C = "\/" ((rng (L0 | C)),L) ) ) & ex L0 being T-Sequence st
( b2 = last L0 & dom L0 = succ O & L0 . {} = x & ( for C being Ordinal st succ C in succ O holds
L0 . (succ C) = f . (L0 . C) ) & ( for C being Ordinal st C in succ O & C <> {} & C is limit_ordinal holds
L0 . C = "\/" ((rng (L0 | C)),L) ) ) holds
b1 = b2 ) ) ; ::_thesis: verum
end;
func(f,O) -. x ->  set  means :Def5: :: KNASTER:def 5
 ex L0 being T-Sequence st
( it = last L0 & dom L0 = succ O & L0 . {} = x & ( for C being Ordinal st succ C in succ O holds
L0 . (succ C) = f . (L0 . C) ) & ( for C being Ordinal st C in succ O & C <> {} & C is limit_ordinal holds
L0 . C = "/\" ((rng (L0 | C)),L) ) );
correctness
existence
ex b1 being set ex L0 being T-Sequence st
( b1 = last L0 & dom L0 = succ O & L0 . {} = x & ( for C being Ordinal st succ C in succ O holds
L0 . (succ C) = f . (L0 . C) ) & ( for C being Ordinal st C in succ O & C <> {} & C is limit_ordinal holds
L0 . C = "/\" ((rng (L0 | C)),L) ) );
uniqueness
for b1, b2 being set st ex L0 being T-Sequence st
( b1 = last L0 & dom L0 = succ O & L0 . {} = x & ( for C being Ordinal st succ C in succ O holds
L0 . (succ C) = f . (L0 . C) ) & ( for C being Ordinal st C in succ O & C <> {} & C is limit_ordinal holds
L0 . C = "/\" ((rng (L0 | C)),L) ) ) & ex L0 being T-Sequence st
( b2 = last L0 & dom L0 = succ O & L0 . {} = x & ( for C being Ordinal st succ C in succ O holds
L0 . (succ C) = f . (L0 . C) ) & ( for C being Ordinal st C in succ O & C <> {} & C is limit_ordinal holds
L0 . C = "/\" ((rng (L0 | C)),L) ) ) holds
b1 = b2;
proof
deffunc H1( Ordinal, T-Sequence) ->  Element of the carrier of L = "/\" ((rng $2),L);
deffunc H2( Ordinal, set ) ->  set = f . $2;
 ( ex z being set ex S being T-Sequence st
( z = last S & dom S = succ O & S . {} = x & ( for C being Ordinal st succ C in succ O holds
S . (succ C) = H2(C,S . C) ) & ( for C being Ordinal st C in succ O & C <> {} & C is limit_ordinal holds
S . C = H1(C,S | C) ) ) & ( for x1, x2 being set st ex L0 being T-Sequence st
( x1 = last L0 & dom L0 = succ O & L0 . {} = x & ( for C being Ordinal st succ C in succ O holds
L0 . (succ C) = H2(C,L0 . C) ) & ( for C being Ordinal st C in succ O & C <> {} & C is limit_ordinal holds
L0 . C = H1(C,L0 | C) ) ) & ex L0 being T-Sequence st
( x2 = last L0 & dom L0 = succ O & L0 . {} = x & ( for C being Ordinal st succ C in succ O holds
L0 . (succ C) = H2(C,L0 . C) ) & ( for C being Ordinal st C in succ O & C <> {} & C is limit_ordinal holds
L0 . C = H1(C,L0 | C) ) ) holds
x1 = x2 ) ) from ORDINAL2:sch_7();
hence  ( ex b1 being set ex L0 being T-Sequence st
( b1 = last L0 & dom L0 = succ O & L0 . {} = x & ( for C being Ordinal st succ C in succ O holds
L0 . (succ C) = f . (L0 . C) ) & ( for C being Ordinal st C in succ O & C <> {} & C is limit_ordinal holds
L0 . C = "/\" ((rng (L0 | C)),L) ) ) & ( for b1, b2 being set st ex L0 being T-Sequence st
( b1 = last L0 & dom L0 = succ O & L0 . {} = x & ( for C being Ordinal st succ C in succ O holds
L0 . (succ C) = f . (L0 . C) ) & ( for C being Ordinal st C in succ O & C <> {} & C is limit_ordinal holds
L0 . C = "/\" ((rng (L0 | C)),L) ) ) & ex L0 being T-Sequence st
( b2 = last L0 & dom L0 = succ O & L0 . {} = x & ( for C being Ordinal st succ C in succ O holds
L0 . (succ C) = f . (L0 . C) ) & ( for C being Ordinal st C in succ O & C <> {} & C is limit_ordinal holds
L0 . C = "/\" ((rng (L0 | C)),L) ) ) holds
b1 = b2 ) ) ; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines +. KNASTER:def_4_:_
 for L being Lattice
for f being Function of the carrier of L, the carrier of L
for x being Element of L
for O being Ordinal
for b5 being set holds
( b5 = (f,O) +. x iff ex L0 being T-Sequence st
( b5 = last L0 & dom L0 = succ O & L0 . {} = x & ( for C being Ordinal st succ C in succ O holds
L0 . (succ C) = f . (L0 . C) ) & ( for C being Ordinal st C in succ O & C <> {} & C is limit_ordinal holds
L0 . C = "\/" ((rng (L0 | C)),L) ) ) );

:: deftheorem Def5 defines -. KNASTER:def_5_:_
 for L being Lattice
for f being Function of the carrier of L, the carrier of L
for x being Element of L
for O being Ordinal
for b5 being set holds
( b5 = (f,O) -. x iff ex L0 being T-Sequence st
( b5 = last L0 & dom L0 = succ O & L0 . {} = x & ( for C being Ordinal st succ C in succ O holds
L0 . (succ C) = f . (L0 . C) ) & ( for C being Ordinal st C in succ O & C <> {} & C is limit_ordinal holds
L0 . C = "/\" ((rng (L0 | C)),L) ) ) );


theorem Th13: :: KNASTER:13
for L being Lattice
for f being Function of the carrier of L, the carrier of L
for x being Element of L holds (f,{}) +. x = x
proof
let L be Lattice; ::_thesis: for f being Function of the carrier of L, the carrier of L
for x being Element of L holds (f,{}) +. x = x
let f be Function of the carrier of L, the carrier of L; ::_thesis: for x being Element of L holds (f,{}) +. x = x
let x be Element of L; ::_thesis: (f,{}) +. x = x
deffunc H1( Ordinal, set ) ->  set = f . $2;
deffunc H2( Ordinal, T-Sequence) ->  Element of the carrier of L = "\/" ((rng $2),L);
deffunc H3( Ordinal) ->  set = (f,$1) +. x;
A1: for O being Ordinal
for y being set holds
( y = H3(O) iff ex L0 being T-Sequence st
( y = last L0 & dom L0 = succ O & L0 . {} = x & ( for C being Ordinal st succ C in succ O holds
L0 . (succ C) = H1(C,L0 . C) ) & ( for C being Ordinal st C in succ O & C <> {} & C is limit_ordinal holds
L0 . C = H2(C,L0 | C) ) ) ) by Def4;
thus  H3( {} ) = x from ORDINAL2:sch_8(A1); ::_thesis: verum
end;

theorem Th14: :: KNASTER:14
for L being Lattice
for f being Function of the carrier of L, the carrier of L
for x being Element of L holds (f,{}) -. x = x
proof
let L be Lattice; ::_thesis: for f being Function of the carrier of L, the carrier of L
for x being Element of L holds (f,{}) -. x = x
let f be Function of the carrier of L, the carrier of L; ::_thesis: for x being Element of L holds (f,{}) -. x = x
let x be Element of L; ::_thesis: (f,{}) -. x = x
deffunc H1( Ordinal, set ) ->  set = f . $2;
deffunc H2( Ordinal, T-Sequence) ->  Element of the carrier of L = "/\" ((rng $2),L);
deffunc H3( Ordinal) ->  set = (f,$1) -. x;
A1: for O being Ordinal
for y being set holds
( y = H3(O) iff ex L0 being T-Sequence st
( y = last L0 & dom L0 = succ O & L0 . {} = x & ( for C being Ordinal st succ C in succ O holds
L0 . (succ C) = H1(C,L0 . C) ) & ( for C being Ordinal st C in succ O & C <> {} & C is limit_ordinal holds
L0 . C = H2(C,L0 | C) ) ) ) by Def5;
thus  H3( {} ) = x from ORDINAL2:sch_8(A1); ::_thesis: verum
end;

theorem Th15: :: KNASTER:15
for L being Lattice
for f being Function of the carrier of L, the carrier of L
for x being Element of L
for O being Ordinal holds (f,(succ O)) +. x = f . ((f,O) +. x)
proof
let L be Lattice; ::_thesis: for f being Function of the carrier of L, the carrier of L
for x being Element of L
for O being Ordinal holds (f,(succ O)) +. x = f . ((f,O) +. x)
let f be Function of the carrier of L, the carrier of L; ::_thesis: for x being Element of L
for O being Ordinal holds (f,(succ O)) +. x = f . ((f,O) +. x)
let x be Element of L; ::_thesis: for O being Ordinal holds (f,(succ O)) +. x = f . ((f,O) +. x)
let O be Ordinal; ::_thesis: (f,(succ O)) +. x = f . ((f,O) +. x)
deffunc H1( Ordinal, set ) ->  set = f . $2;
deffunc H2( Ordinal, T-Sequence) ->  Element of the carrier of L = "\/" ((rng $2),L);
deffunc H3( Ordinal) ->  set = (f,$1) +. x;
A1: for O being Ordinal
for y being set holds
( y = H3(O) iff ex L0 being T-Sequence st
( y = last L0 & dom L0 = succ O & L0 . {} = x & ( for C being Ordinal st succ C in succ O holds
L0 . (succ C) = H1(C,L0 . C) ) & ( for C being Ordinal st C in succ O & C <> {} & C is limit_ordinal holds
L0 . C = H2(C,L0 | C) ) ) ) by Def4;
 for O being Ordinal holds H3( succ O) = H1(O,H3(O)) from ORDINAL2:sch_9(A1);
hence  (f,(succ O)) +. x = f . ((f,O) +. x) ; ::_thesis: verum
end;

theorem Th16: :: KNASTER:16
for L being Lattice
for f being Function of the carrier of L, the carrier of L
for x being Element of L
for O being Ordinal holds (f,(succ O)) -. x = f . ((f,O) -. x)
proof
let L be Lattice; ::_thesis: for f being Function of the carrier of L, the carrier of L
for x being Element of L
for O being Ordinal holds (f,(succ O)) -. x = f . ((f,O) -. x)
let f be Function of the carrier of L, the carrier of L; ::_thesis: for x being Element of L
for O being Ordinal holds (f,(succ O)) -. x = f . ((f,O) -. x)
let x be Element of L; ::_thesis: for O being Ordinal holds (f,(succ O)) -. x = f . ((f,O) -. x)
let O be Ordinal; ::_thesis: (f,(succ O)) -. x = f . ((f,O) -. x)
deffunc H1( Ordinal, set ) ->  set = f . $2;
deffunc H2( Ordinal, T-Sequence) ->  Element of the carrier of L = "/\" ((rng $2),L);
deffunc H3( Ordinal) ->  set = (f,$1) -. x;
A1: for O being Ordinal
for y being set holds
( y = H3(O) iff ex L0 being T-Sequence st
( y = last L0 & dom L0 = succ O & L0 . {} = x & ( for C being Ordinal st succ C in succ O holds
L0 . (succ C) = H1(C,L0 . C) ) & ( for C being Ordinal st C in succ O & C <> {} & C is limit_ordinal holds
L0 . C = H2(C,L0 | C) ) ) ) by Def5;
 for O being Ordinal holds H3( succ O) = H1(O,H3(O)) from ORDINAL2:sch_9(A1);
hence  (f,(succ O)) -. x = f . ((f,O) -. x) ; ::_thesis: verum
end;

theorem Th17: :: KNASTER:17
for L being Lattice
for f being Function of the carrier of L, the carrier of L
for x being Element of L
for O being Ordinal
for T being T-Sequence st O <> {} & O is limit_ordinal & dom T = O & ( for A being Ordinal st A in O holds
T . A = (f,A) +. x ) holds
(f,O) +. x = "\/" ((rng T),L)
proof
let L be Lattice; ::_thesis: for f being Function of the carrier of L, the carrier of L
for x being Element of L
for O being Ordinal
for T being T-Sequence st O <> {} & O is limit_ordinal & dom T = O & ( for A being Ordinal st A in O holds
T . A = (f,A) +. x ) holds
(f,O) +. x = "\/" ((rng T),L)
let f be Function of the carrier of L, the carrier of L; ::_thesis: for x being Element of L
for O being Ordinal
for T being T-Sequence st O <> {} & O is limit_ordinal & dom T = O & ( for A being Ordinal st A in O holds
T . A = (f,A) +. x ) holds
(f,O) +. x = "\/" ((rng T),L)
let x be Element of L; ::_thesis: for O being Ordinal
for T being T-Sequence st O <> {} & O is limit_ordinal & dom T = O & ( for A being Ordinal st A in O holds
T . A = (f,A) +. x ) holds
(f,O) +. x = "\/" ((rng T),L)
let O be Ordinal; ::_thesis: for T being T-Sequence st O <> {} & O is limit_ordinal & dom T = O & ( for A being Ordinal st A in O holds
T . A = (f,A) +. x ) holds
(f,O) +. x = "\/" ((rng T),L)
let T be T-Sequence; ::_thesis: ( O <> {} & O is limit_ordinal & dom T = O & ( for A being Ordinal st A in O holds
T . A = (f,A) +. x ) implies (f,O) +. x = "\/" ((rng T),L) )
deffunc H1( Ordinal, set ) ->  set = f . $2;
deffunc H2( Ordinal, T-Sequence) ->  Element of the carrier of L = "\/" ((rng $2),L);
deffunc H3( Ordinal) ->  set = (f,$1) +. x;
assume that
A1: ( O <> {} & O is limit_ordinal ) and
A2: dom T = O and
A3: for A being Ordinal st A in O holds
T . A = H3(A) ; ::_thesis: (f,O) +. x = "\/" ((rng T),L)
A4: for O being Ordinal
for y being set holds
( y = H3(O) iff ex L0 being T-Sequence st
( y = last L0 & dom L0 = succ O & L0 . {} = x & ( for C being Ordinal st succ C in succ O holds
L0 . (succ C) = H1(C,L0 . C) ) & ( for C being Ordinal st C in succ O & C <> {} & C is limit_ordinal holds
L0 . C = H2(C,L0 | C) ) ) ) by Def4;
thus  H3(O) = H2(O,T) from ORDINAL2:sch_10(A4, A1, A2, A3); ::_thesis: verum
end;

theorem Th18: :: KNASTER:18
for L being Lattice
for f being Function of the carrier of L, the carrier of L
for x being Element of L
for O being Ordinal
for T being T-Sequence st O <> {} & O is limit_ordinal & dom T = O & ( for A being Ordinal st A in O holds
T . A = (f,A) -. x ) holds
(f,O) -. x = "/\" ((rng T),L)
proof
let L be Lattice; ::_thesis: for f being Function of the carrier of L, the carrier of L
for x being Element of L
for O being Ordinal
for T being T-Sequence st O <> {} & O is limit_ordinal & dom T = O & ( for A being Ordinal st A in O holds
T . A = (f,A) -. x ) holds
(f,O) -. x = "/\" ((rng T),L)
let f be Function of the carrier of L, the carrier of L; ::_thesis: for x being Element of L
for O being Ordinal
for T being T-Sequence st O <> {} & O is limit_ordinal & dom T = O & ( for A being Ordinal st A in O holds
T . A = (f,A) -. x ) holds
(f,O) -. x = "/\" ((rng T),L)
let x be Element of L; ::_thesis: for O being Ordinal
for T being T-Sequence st O <> {} & O is limit_ordinal & dom T = O & ( for A being Ordinal st A in O holds
T . A = (f,A) -. x ) holds
(f,O) -. x = "/\" ((rng T),L)
let O be Ordinal; ::_thesis: for T being T-Sequence st O <> {} & O is limit_ordinal & dom T = O & ( for A being Ordinal st A in O holds
T . A = (f,A) -. x ) holds
(f,O) -. x = "/\" ((rng T),L)
let T be T-Sequence; ::_thesis: ( O <> {} & O is limit_ordinal & dom T = O & ( for A being Ordinal st A in O holds
T . A = (f,A) -. x ) implies (f,O) -. x = "/\" ((rng T),L) )
deffunc H1( Ordinal, set ) ->  set = f . $2;
deffunc H2( Ordinal, T-Sequence) ->  Element of the carrier of L = "/\" ((rng $2),L);
deffunc H3( Ordinal) ->  set = (f,$1) -. x;
assume that
A1: ( O <> {} & O is limit_ordinal ) and
A2: dom T = O and
A3: for A being Ordinal st A in O holds
T . A = H3(A) ; ::_thesis: (f,O) -. x = "/\" ((rng T),L)
A4: for O being Ordinal
for y being set holds
( y = H3(O) iff ex L0 being T-Sequence st
( y = last L0 & dom L0 = succ O & L0 . {} = x & ( for C being Ordinal st succ C in succ O holds
L0 . (succ C) = H1(C,L0 . C) ) & ( for C being Ordinal st C in succ O & C <> {} & C is limit_ordinal holds
L0 . C = H2(C,L0 | C) ) ) ) by Def5;
thus  H3(O) = H2(O,T) from ORDINAL2:sch_10(A4, A1, A2, A3); ::_thesis: verum
end;

theorem :: KNASTER:19
for n being Element of NAT
for L being Lattice
for f being Function of the carrier of L, the carrier of L
for x being Element of L holds (iter (f,n)) . x = (f,n) +. x
proof
let n be Element of NAT ; ::_thesis: for L being Lattice
for f being Function of the carrier of L, the carrier of L
for x being Element of L holds (iter (f,n)) . x = (f,n) +. x
let L be Lattice; ::_thesis: for f being Function of the carrier of L, the carrier of L
for x being Element of L holds (iter (f,n)) . x = (f,n) +. x
let f be Function of the carrier of L, the carrier of L; ::_thesis: for x being Element of L holds (iter (f,n)) . x = (f,n) +. x
let x be Element of L; ::_thesis: (iter (f,n)) . x = (f,n) +. x
defpred S1[ Element of 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__::_thesis:_for_n_being_Element_of_NAT_st_S1[n]_holds_
S1[n_+_1]
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A4: S1[n] ; ::_thesis: S1[n + 1]
 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 n)) +. x by Th15
.= (f,(n + 1)) +. x by NAT_1:38 ;
hence  S1[n + 1] ; ::_thesis: verum
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: S1[ 0 ] ;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A6, A3);
hence  (iter (f,n)) . x = (f,n) +. x ; ::_thesis: verum
end;

theorem :: KNASTER:20
for n being Element of NAT
for L being Lattice
for f being Function of the carrier of L, the carrier of L
for x being Element of L holds (iter (f,n)) . x = (f,n) -. x
proof
let n be Element of NAT ; ::_thesis: for L being Lattice
for f being Function of the carrier of L, the carrier of L
for x being Element of L holds (iter (f,n)) . x = (f,n) -. x
let L be Lattice; ::_thesis: for f being Function of the carrier of L, the carrier of L
for x being Element of L holds (iter (f,n)) . x = (f,n) -. x
let f be Function of the carrier of L, the carrier of L; ::_thesis: for x being Element of L holds (iter (f,n)) . x = (f,n) -. x
let x be Element of L; ::_thesis: (iter (f,n)) . x = (f,n) -. x
defpred S1[ Element of 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__::_thesis:_for_n_being_Element_of_NAT_st_S1[n]_holds_
S1[n_+_1]
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A4: S1[n] ; ::_thesis: S1[n + 1]
 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 n)) -. x by Th16
.= (f,(n + 1)) -. x by NAT_1:38 ;
hence  S1[n + 1] ; ::_thesis: verum
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: S1[ 0 ] ;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A6, A3);
hence  (iter (f,n)) . x = (f,n) -. x ; ::_thesis: verum
end;

definition
let L be Lattice;
let f be UnOp of the carrier of L;
let a be Element of L;
let O be Ordinal;
:: original: +.
redefine func(f,O) +. a ->  Element of L;
coherence
 (f,O) +. a is Element of L
proof
deffunc H1( Ordinal) ->  set = (f,$1) +. a;
defpred S1[ Ordinal] means (f,$1) +. a is Element of L;
A1: now__::_thesis:_for_O1_being_Ordinal_st_S1[O1]_holds_
S1[_succ_O1]
let O1 be Ordinal; ::_thesis: ( S1[O1] implies S1[ succ O1] )
assume  S1[O1] ; ::_thesis: S1[ succ O1]
then reconsider fa = (f,O1) +. a as Element of L ;
 f . fa = (f,(succ O1)) +. a by Th15;
hence  S1[ succ O1] ; ::_thesis: verum
end;
A2: now__::_thesis:_for_O1_being_Ordinal_st_O1_<>_{}_&_O1_is_limit_ordinal_&_(_for_O2_being_Ordinal_st_O2_in_O1_holds_
S1[O2]_)_holds_
S1[O1]
let O1 be Ordinal; ::_thesis: ( O1 <> {} & O1 is limit_ordinal & ( for O2 being Ordinal st O2 in O1 holds
S1[O2] ) implies S1[O1] )
assume that
A3: ( O1 <> {} & O1 is limit_ordinal ) and
 for O2 being Ordinal st O2 in O1 holds
S1[O2] ; ::_thesis: S1[O1]
consider Ls being T-Sequence such that
A4: ( dom Ls = O1 & ( for O2 being Ordinal st O2 in O1 holds
Ls . O2 = H1(O2) ) ) from ORDINAL2:sch_2();
 (f,O1) +. a = "\/" ((rng Ls),L) by A3, A4, Th17;
hence  S1[O1] ; ::_thesis: verum
end;
A5: S1[ {} ] by Th13;
 for O being Ordinal holds S1[O] from ORDINAL2:sch_1(A5, A1, A2);
hence  (f,O) +. a is Element of L ; ::_thesis: verum
end;
end;

definition
let L be Lattice;
let f be UnOp of the carrier of L;
let a be Element of L;
let O be Ordinal;
:: original: -.
redefine func(f,O) -. a ->  Element of L;
coherence
 (f,O) -. a is Element of L
proof
deffunc H1( Ordinal) ->  set = (f,$1) -. a;
defpred S1[ Ordinal] means (f,$1) -. a is Element of L;
A1: now__::_thesis:_for_O1_being_Ordinal_st_S1[O1]_holds_
S1[_succ_O1]
let O1 be Ordinal; ::_thesis: ( S1[O1] implies S1[ succ O1] )
assume  S1[O1] ; ::_thesis: S1[ succ O1]
then reconsider fa = (f,O1) -. a as Element of L ;
 f . fa = (f,(succ O1)) -. a by Th16;
hence  S1[ succ O1] ; ::_thesis: verum
end;
A2: now__::_thesis:_for_O1_being_Ordinal_st_O1_<>_{}_&_O1_is_limit_ordinal_&_(_for_O2_being_Ordinal_st_O2_in_O1_holds_
S1[O2]_)_holds_
S1[O1]
let O1 be Ordinal; ::_thesis: ( O1 <> {} & O1 is limit_ordinal & ( for O2 being Ordinal st O2 in O1 holds
S1[O2] ) implies S1[O1] )
assume that
A3: ( O1 <> {} & O1 is limit_ordinal ) and
 for O2 being Ordinal st O2 in O1 holds
S1[O2] ; ::_thesis: S1[O1]
consider Ls being T-Sequence such that
A4: ( dom Ls = O1 & ( for O2 being Ordinal st O2 in O1 holds
Ls . O2 = H1(O2) ) ) from ORDINAL2:sch_2();
 (f,O1) -. a = "/\" ((rng Ls),L) by A3, A4, Th18;
hence  S1[O1] ; ::_thesis: verum
end;
A5: S1[ {} ] by Th14;
 for O being Ordinal holds S1[O] from ORDINAL2:sch_1(A5, A1, A2);
hence  (f,O) -. a is Element of L ; ::_thesis: verum
end;
end;

definition
let L be non empty LattStr ;
let P be Subset of L;
attrP is with_suprema  means :Def6: :: KNASTER:def 6
 for x, y being Element of L st x in P & y in P holds
ex z being Element of L st
( z in P & x [= z & y [= z & ( for z9 being Element of L st z9 in P & x [= z9 & y [= z9 holds
z [= z9 ) );
attrP is with_infima  means :Def7: :: KNASTER:def 7
 for x, y being Element of L st x in P & y in P holds
ex z being Element of L st
( z in P & z [= x & z [= y & ( for z9 being Element of L st z9 in P & z9 [= x & z9 [= y holds
z9 [= z ) );
end;

:: deftheorem Def6 defines with_suprema KNASTER:def_6_:_
 for L being non empty LattStr
for P being Subset of L holds
( P is with_suprema iff for x, y being Element of L st x in P & y in P holds
ex z being Element of L st
( z in P & x [= z & y [= z & ( for z9 being Element of L st z9 in P & x [= z9 & y [= z9 holds
z [= z9 ) ) );

:: deftheorem Def7 defines with_infima KNASTER:def_7_:_
 for L being non empty LattStr
for P being Subset of L holds
( P is with_infima iff for x, y being Element of L st x in P & y in P holds
ex z being Element of L st
( z in P & z [= x & z [= y & ( for z9 being Element of L st z9 in P & z9 [= x & z9 [= y holds
z9 [= z ) ) );

registration
let L be Lattice;
cluster non empty with_suprema with_infima for Element of bool the carrier of L;
existence
 ex b1 being Subset of L st
( not b1 is empty & b1 is with_suprema & b1 is with_infima )
proof
 the carrier of L c= the carrier of L ;
then reconsider P = the carrier of L as Subset of L ;
take  P ; ::_thesis: ( not P is empty & P is with_suprema & P is with_infima )
thus  not P is empty ; ::_thesis: ( P is with_suprema & P is with_infima )
thus  P is with_suprema ::_thesis: P is with_infima
proof
let x, y be Element of L; :: according to KNASTER:def_6 ::_thesis: ( x in P & y in P implies ex z being Element of L st
( z in P & x [= z & y [= z & ( for z9 being Element of L st z9 in P & x [= z9 & y [= z9 holds
z [= z9 ) ) )
assume that
 x in P and
 y in P ; ::_thesis: ex z being Element of L st
( z in P & x [= z & y [= z & ( for z9 being Element of L st z9 in P & x [= z9 & y [= z9 holds
z [= z9 ) )
take z = x "\/" y; ::_thesis: ( z in P & x [= z & y [= z & ( for z9 being Element of L st z9 in P & x [= z9 & y [= z9 holds
z [= z9 ) )
thus  z in P ; ::_thesis: ( x [= z & y [= z & ( for z9 being Element of L st z9 in P & x [= z9 & y [= z9 holds
z [= z9 ) )
thus  ( x [= z & y [= z ) by LATTICES:5; ::_thesis: for z9 being Element of L st z9 in P & x [= z9 & y [= z9 holds
z [= z9
let z9 be Element of L; ::_thesis: ( z9 in P & x [= z9 & y [= z9 implies z [= z9 )
assume that
 z9 in P and
A1: ( x [= z9 & y [= z9 ) ; ::_thesis: z [= z9
thus  z [= z9 by A1, BOOLEALG:5; ::_thesis: verum
end;
let x, y be Element of L; :: according to KNASTER:def_7 ::_thesis: ( x in P & y in P implies ex z being Element of L st
( z in P & z [= x & z [= y & ( for z9 being Element of L st z9 in P & z9 [= x & z9 [= y holds
z9 [= z ) ) )
assume that
 x in P and
 y in P ; ::_thesis: ex z being Element of L st
( z in P & z [= x & z [= y & ( for z9 being Element of L st z9 in P & z9 [= x & z9 [= y holds
z9 [= z ) )
take z = x "/\" y; ::_thesis: ( z in P & z [= x & z [= y & ( for z9 being Element of L st z9 in P & z9 [= x & z9 [= y holds
z9 [= z ) )
thus  z in P ; ::_thesis: ( z [= x & z [= y & ( for z9 being Element of L st z9 in P & z9 [= x & z9 [= y holds
z9 [= z ) )
thus  ( z [= x & z [= y ) by LATTICES:6; ::_thesis: for z9 being Element of L st z9 in P & z9 [= x & z9 [= y holds
z9 [= z
let z9 be Element of L; ::_thesis: ( z9 in P & z9 [= x & z9 [= y implies z9 [= z )
assume that
 z9 in P and
A2: ( z9 [= x & z9 [= y ) ; ::_thesis: z9 [= z
thus  z9 [= z by A2, BOOLEALG:6; ::_thesis: verum
end;
end;

definition
let L be Lattice;
let P be non empty with_suprema with_infima Subset of L;
func latt P ->  strict Lattice means :Def8: :: KNASTER:def 8
( the carrier of it = P & ( for x, y being Element of it ex x9, y9 being Element of L st
( x = x9 & y = y9 & ( x [= y implies x9 [= y9 ) & ( x9 [= y9 implies x [= y ) ) ) );
existence
 ex b1 being strict Lattice st
( the carrier of b1 = P & ( for x, y being Element of b1 ex x9, y9 being Element of L st
( x = x9 & y = y9 & ( x [= y implies x9 [= y9 ) & ( x9 [= y9 implies x [= y ) ) ) )
proof
set cL = the carrier of L;
set LL = LattRel L;
set LR = (LattRel L) |_2 P;
reconsider LR = (LattRel L) |_2 P as Relation of P by XBOOLE_1:17;
 field (LattRel L) = the carrier of L by FILTER_1:32;
then A1: LattRel L is_reflexive_in the carrier of L by RELAT_2:def_9;
A2: field LR = P
proof
thus  field LR c= P by WELLORD1:13; :: according to XBOOLE_0:def_10 ::_thesis: P c= field LR
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P or x in field LR )
assume  x in P ; ::_thesis: x in field LR
then  ( [x,x] in [:P,P:] & [x,x] in LattRel L ) by A1, RELAT_2:def_1, ZFMISC_1:87;
then  [x,x] in LR by XBOOLE_0:def_4;
hence  x in field LR by RELAT_1:15; ::_thesis: verum
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 = LR as Order of P by A4, PARTFUN1:def_2, WELLORD1:15, WELLORD1:17, WELLORD1:18;
set RS = RelStr(# P,LR #);
take IT = latt RelStr(# P,LR #); ::_thesis: ( the carrier of IT = P & ( for x, y being Element of IT ex x9, y9 being Element of L st
( x = x9 & y = y9 & ( x [= y implies x9 [= y9 ) & ( x9 [= y9 implies x [= y ) ) ) )
A7: RelStr(# P,LR #) is with_suprema
proof
let x, y be Element of RelStr(# P,LR #); :: according to LATTICE3:def_10 ::_thesis: ex b1 being Element of the carrier of RelStr(# P,LR #) st
( x <= b1 & y <= b1 & ( for b2 being Element of the carrier of RelStr(# P,LR #) holds
( not x <= b2 or not y <= b2 or b1 <= b2 ) ) )
 ( x in P & y in P ) ;
then reconsider xL = x, yL = y as Element of L ;
consider zL being Element of L such that
A8: zL in P and
A9: xL [= zL and
A10: yL [= zL and
A11: for z9 being Element of L st z9 in P & xL [= z9 & yL [= z9 holds
zL [= z9 by Def6;
 ( [yL,zL] in [:P,P:] & [yL,zL] in LattRel L ) 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 RelStr(# P,LR #) by A8;
take  z ; ::_thesis: ( x <= z & y <= z & ( for b1 being Element of the carrier of RelStr(# P,LR #) holds
( not x <= b1 or not y <= b1 or z <= b1 ) ) )
 ( [xL,zL] in [:P,P:] & [xL,zL] in LattRel L ) 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; ::_thesis: for b1 being Element of the carrier of RelStr(# P,LR #) holds
( not x <= b1 or not y <= b1 or z <= b1 )
let z9 be Element of RelStr(# P,LR #); ::_thesis: ( not x <= z9 or not y <= z9 or z <= z9 )
assume that
A13: x <= z9 and
A14: y <= z9 ; ::_thesis: z <= 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 LattRel L 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 LattRel L by XBOOLE_0:def_4;
then  xL [= z9L by FILTER_1:31;
then  zL [= z9L by A11, A15;
then A16: [zL,z9L] in LattRel L 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  z <= z9 by ORDERS_2:def_5; ::_thesis: verum
end;
A17: RelStr(# P,LR #) is with_infima
proof
let x, y be Element of RelStr(# P,LR #); :: according to LATTICE3:def_11 ::_thesis: ex b1 being Element of the carrier of RelStr(# P,LR #) st
( b1 <= x & b1 <= y & ( for b2 being Element of the carrier of RelStr(# P,LR #) holds
( not b2 <= x or not b2 <= y or b2 <= b1 ) ) )
 ( x in P & y in P ) ;
then reconsider xL = x, yL = y as Element of L ;
consider zL being Element of L such that
A18: zL in P and
A19: zL [= xL and
A20: zL [= yL and
A21: for z9 being Element of L st z9 in P & z9 [= xL & z9 [= yL holds
z9 [= zL by Def7;
 ( [zL,yL] in [:P,P:] & [zL,yL] in LattRel L ) 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 RelStr(# P,LR #) by A18;
take  z ; ::_thesis: ( z <= x & z <= y & ( for b1 being Element of the carrier of RelStr(# P,LR #) holds
( not b1 <= x or not b1 <= y or b1 <= z ) ) )
 ( [zL,xL] in [:P,P:] & [zL,xL] in LattRel L ) 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; ::_thesis: for b1 being Element of the carrier of RelStr(# P,LR #) holds
( not b1 <= x or not b1 <= y or b1 <= z )
let z9 be Element of RelStr(# P,LR #); ::_thesis: ( not z9 <= x or not z9 <= y or z9 <= z )
assume that
A23: z9 <= x and
A24: z9 <= y ; ::_thesis: z9 <= z
 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 LattRel L 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 LattRel L by XBOOLE_0:def_4;
then  z9L [= xL by FILTER_1:31;
then  z9L [= zL by A21, A25;
then A26: [z9L,zL] in LattRel L 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  z9 <= z by ORDERS_2:def_5; ::_thesis: verum
end;
A27: RelStr(# P,LR #) is Poset by A3, A6, A5, ORDERS_2:def_2, ORDERS_2:def_3, ORDERS_2:def_4;
then A28: RelStr(# P,LR #) = 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; ::_thesis: for x, y being Element of IT ex x9, y9 being Element of L st
( x = x9 & y = y9 & ( x [= y implies x9 [= y9 ) & ( x9 [= y9 implies x [= y ) )
let x, y be Element of IT; ::_thesis: ex x9, y9 being Element of L st
( x = x9 & y = y9 & ( x [= y implies x9 [= y9 ) & ( x9 [= y9 implies x [= y ) )
 ( x in P & y in P ) by A28;
then reconsider x9 = x, y9 = y as Element of L ;
take  x9 ; ::_thesis: ex y9 being Element of L st
( x = x9 & y = y9 & ( x [= y implies x9 [= y9 ) & ( x9 [= y9 implies x [= y ) )
take  y9 ; ::_thesis: ( x = x9 & y = y9 & ( x [= y implies x9 [= y9 ) & ( x9 [= y9 implies x [= y ) )
thus  ( x = x9 & y = y9 ) ; ::_thesis: ( ( x [= y implies x9 [= y9 ) & ( x9 [= y9 implies x [= y ) )
hereby  ::_thesis: ( x9 [= y9 implies x [= y )
assume  x [= y ; ::_thesis: x9 [= y9
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; ::_thesis: verum
end;
assume  x9 [= y9 ; ::_thesis: x [= y
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  x [= y by FILTER_1:31; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict Lattice st the carrier of b1 = P & ( for x, y being Element of b1 ex x9, y9 being Element of L st
( x = x9 & y = y9 & ( x [= y implies x9 [= y9 ) & ( x9 [= y9 implies x [= y ) ) ) & the carrier of b2 = P & ( for x, y being Element of b2 ex x9, y9 being Element of L st
( x = x9 & y = y9 & ( x [= y implies x9 [= y9 ) & ( x9 [= y9 implies x [= y ) ) ) holds
b1 = b2
proof
let it1, it2 be strict Lattice; ::_thesis: ( the carrier of it1 = P & ( for x, y being Element of it1 ex x9, y9 being Element of L st
( x = x9 & y = y9 & ( x [= y implies x9 [= y9 ) & ( x9 [= y9 implies x [= y ) ) ) & the carrier of it2 = P & ( for x, y being Element of it2 ex x9, y9 being Element of L st
( x = x9 & y = y9 & ( x [= y implies x9 [= y9 ) & ( x9 [= y9 implies x [= y ) ) ) implies it1 = it2 )
assume that
A30: the carrier of it1 = P and
A31: for x, y being Element of it1 ex x9, y9 being Element of L st
( x = x9 & y = y9 & ( x [= y implies x9 [= y9 ) & ( x9 [= y9 implies x [= y ) ) and
A32: the carrier of it2 = P and
A33: for x, y being Element of it2 ex x9, y9 being Element of L st
( x = x9 & y = y9 & ( x [= y implies x9 [= y9 ) & ( x9 [= y9 implies x [= y ) ) ; ::_thesis: it1 = it2
A34: LattRel it2 =  {  [p,q] where p, q is Element of it2 : p [= q  }  by FILTER_1:def_8;
A35: LattRel it1 =  {  [p,q] where p, q is Element of it1 : p [= q  }  by FILTER_1:def_8;
now__::_thesis:_for_a_being_set_holds_
(_(_a_in_LattRel_it1_implies_a_in_LattRel_it2_)_&_(_a_in_LattRel_it2_implies_a_in_LattRel_it1_)_)
let a be set ; ::_thesis: ( ( a in LattRel it1 implies a in LattRel it2 ) & ( a in LattRel it2 implies a in LattRel it1 ) )
hereby  ::_thesis: ( a in LattRel it2 implies a in LattRel it1 )
assume  a in LattRel it1 ; ::_thesis: a in LattRel it2
then consider p1, q1 being Element of it1 such that
A36: ( a = [p1,q1] & p1 [= q1 ) by A35;
reconsider p1 = p1, q1 = q1 as Element of it1 ;
reconsider p2 = p1, q2 = q1 as Element of it2 by A30, A32;
 ( ex pl1, ql1 being Element of L st
( p1 = pl1 & q1 = ql1 & ( p1 [= q1 implies pl1 [= ql1 ) & ( pl1 [= ql1 implies p1 [= q1 ) ) & ex pl2, ql2 being Element of L st
( p2 = pl2 & q2 = ql2 & ( p2 [= q2 implies pl2 [= ql2 ) & ( pl2 [= ql2 implies p2 [= q2 ) ) ) by A31, A33;
hence  a in LattRel it2 by A34, A36; ::_thesis: verum
end;
assume  a in LattRel it2 ; ::_thesis: a in LattRel it1
then consider p1, q1 being Element of it2 such that
A37: ( a = [p1,q1] & p1 [= q1 ) by A34;
reconsider p1 = p1, q1 = q1 as Element of it2 ;
reconsider p2 = p1, q2 = q1 as Element of it1 by A30, A32;
 ( ex pl1, ql1 being Element of L st
( p1 = pl1 & q1 = ql1 & ( p1 [= q1 implies pl1 [= ql1 ) & ( pl1 [= ql1 implies p1 [= q1 ) ) & ex pl2, ql2 being Element of L st
( p2 = pl2 & q2 = ql2 & ( p2 [= q2 implies pl2 [= ql2 ) & ( pl2 [= ql2 implies p2 [= q2 ) ) ) by A31, A33;
hence  a in LattRel it1 by A35, A37; ::_thesis: verum
end;
then A38: LattRel it1 = LattRel it2 by TARSKI:1;
 ( LattPOSet it1 = RelStr(# the carrier of it1,(LattRel it1) #) & LattPOSet it2 = RelStr(# the carrier of it2,(LattRel it2) #) ) ;
hence  it1 = it2 by A30, A32, A38, LATTICE3:6; ::_thesis: verum
end;
end;

:: deftheorem Def8 defines latt KNASTER:def_8_:_
 for L being Lattice
for P being non empty with_suprema with_infima Subset of L
for b3 being strict Lattice holds
( b3 = latt P iff ( the carrier of b3 = P & ( for x, y being Element of b3 ex x9, y9 being Element of L st
( x = x9 & y = y9 & ( x [= y implies x9 [= y9 ) & ( x9 [= y9 implies x [= y ) ) ) ) );

begin

registration
cluster non empty Lattice-like complete  ->  bounded for LattStr ;
coherence
 for b1 being Lattice st b1 is complete holds
b1 is bounded
proof
let L be Lattice; ::_thesis: ( L is complete implies L is bounded )
assume  L is complete ; ::_thesis: L is bounded
then  ( L is 0_Lattice & L is 1_Lattice ) by LATTICE3:49, LATTICE3:50;
hence  L is bounded ; ::_thesis: verum
end;
end;


theorem Th21: :: KNASTER:21
for L being complete Lattice
for f being monotone UnOp of L ex a being Element of L st a is_a_fixpoint_of f
proof
let L be complete Lattice; ::_thesis: for f being monotone UnOp of L ex a being Element of L st a is_a_fixpoint_of f
let f be monotone UnOp of L; ::_thesis: ex a being Element of L st a is_a_fixpoint_of f
set H =  {  h where h is Element of L : h [= f . h  }  ;
set fH =  {  (f . h) where h is Element of L : h [= f . h  }  ;
set uH = "\/" ( {  h where h is Element of L : h [= f . h  }  ,L);
set fuH = "\/" ( {  (f . h) where h is Element of L : h [= f . h  }  ,L);
take  "\/" ( {  h where h is Element of L : h [= f . h  }  ,L) ; ::_thesis: "\/" ( {  h where h is Element of L : h [= f . h  }  ,L) is_a_fixpoint_of f
now__::_thesis:_for_fh_being_Element_of_L_st_fh_in__{__(f_._h)_where_h_is_Element_of_L_:_h_[=_f_._h__}__holds_
fh_[=_f_._("\/"_(_{__h_where_h_is_Element_of_L_:_h_[=_f_._h__}__,L))
let fh be Element of L; ::_thesis: ( fh in  {  (f . h) where h is Element of L : h [= f . h  }  implies fh [= f . ("\/" ( {  h where h is Element of L : h [= f . h  }  ,L)) )
assume  fh in  {  (f . h) where h is Element of L : h [= f . h  }  ; ::_thesis: fh [= f . ("\/" ( {  h where h is Element of L : h [= f . h  }  ,L))
then consider h being Element of L such that
A1: fh = f . h and
A2: h [= f . h ;
 h in  {  h where h is Element of L : h [= f . h  }  by A2;
then  h [= "\/" ( {  h where h is Element of L : h [= f . h  }  ,L) by LATTICE3:38;
hence  fh [= f . ("\/" ( {  h where h is Element of L : h [= f . h  }  ,L)) by A1, QUANTAL1:def_12; ::_thesis: verum
end;
then   {  (f . h) where h is Element of L : h [= f . h  }  is_less_than f . ("\/" ( {  h where h is Element of L : h [= f . h  }  ,L)) by LATTICE3:def_17;
then A3: "\/" ( {  (f . h) where h is Element of L : h [= f . h  }  ,L) [= f . ("\/" ( {  h where h is Element of L : h [= f . h  }  ,L)) by LATTICE3:def_21;
now__::_thesis:_for_a_being_Element_of_L_st_a_in__{__h_where_h_is_Element_of_L_:_h_[=_f_._h__}__holds_
ex_fh_being_Element_of_L_st_
(_a_[=_fh_&_fh_in__{__(f_._h)_where_h_is_Element_of_L_:_h_[=_f_._h__}__)
let a be Element of L; ::_thesis: ( a in  {  h where h is Element of L : h [= f . h  }  implies ex fh being Element of L st
( a [= fh & fh in  {  (f . h) where h is Element of L : h [= f . h  }  ) )
assume  a in  {  h where h is Element of L : h [= f . h  }  ; ::_thesis: ex fh being Element of L st
( a [= fh & fh in  {  (f . h) where h is Element of L : h [= f . h  }  )
then consider h being Element of L such that
A4: ( a = h & h [= f . h ) ;
reconsider fh = f . h as Element of L ;
take fh = fh; ::_thesis: ( a [= fh & fh in  {  (f . h) where h is Element of L : h [= f . h  }  )
thus  ( a [= fh & fh in  {  (f . h) where h is Element of L : h [= f . h  }  ) by A4; ::_thesis: verum
end;
then  "\/" ( {  h where h is Element of L : h [= f . h  }  ,L) [= "\/" ( {  (f . h) where h is Element of L : h [= f . h  }  ,L) by LATTICE3:47;
then A5: "\/" ( {  h where h is Element of L : h [= f . h  }  ,L) [= f . ("\/" ( {  h where h is Element of L : h [= f . h  }  ,L)) by A3, LATTICES:7;
then  f . ("\/" ( {  h where h is Element of L : h [= f . h  }  ,L)) [= f . (f . ("\/" ( {  h where h is Element of L : h [= f . h  }  ,L))) by QUANTAL1:def_12;
then  f . ("\/" ( {  h where h is Element of L : h [= f . h  }  ,L)) in  {  h where h is Element of L : h [= f . h  }  ;
then  f . ("\/" ( {  h where h is Element of L : h [= f . h  }  ,L)) [= "\/" ( {  h where h is Element of L : h [= f . h  }  ,L) by LATTICE3:38;
hence  "\/" ( {  h where h is Element of L : h [= f . h  }  ,L) = f . ("\/" ( {  h where h is Element of L : h [= f . h  }  ,L)) by A5, LATTICES:8; :: according to ABIAN:def_4 ::_thesis: verum
end;

theorem Th22: :: KNASTER:22
for L being complete Lattice
for f being monotone UnOp of L
for a being Element of L st a [= f . a holds
for O being Ordinal holds a [= (f,O) +. a
proof
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 O being Ordinal holds a [= (f,O) +. a
let f be monotone UnOp of L; ::_thesis: for a being Element of L st a [= f . a holds
for O being Ordinal holds a [= (f,O) +. a
let a be Element of L; ::_thesis: ( a [= f . a implies for O being Ordinal holds a [= (f,O) +. a )
defpred S1[ Ordinal] means a [= (f,$1) +. a;
deffunc H1( Ordinal) ->  Element of L = (f,$1) +. a;
A1: now__::_thesis:_for_O1_being_Ordinal_st_O1_<>_{}_&_O1_is_limit_ordinal_&_(_for_O2_being_Ordinal_st_O2_in_O1_holds_
S1[O2]_)_holds_
S1[O1]
let O1 be Ordinal; ::_thesis: ( O1 <> {} & O1 is limit_ordinal & ( for O2 being Ordinal st O2 in O1 holds
S1[O2] ) implies S1[O1] )
assume that
A2: O1 <> {} and
A3: O1 is limit_ordinal and
A4: for O2 being Ordinal st O2 in O1 holds
S1[O2] ; ::_thesis: S1[O1]
consider O2 being set  such that
A5: O2 in O1 by A2, XBOOLE_0:def_1;
reconsider O2 = O2 as Ordinal by A5;
A6: S1[O2] by A4, A5;
consider Ls being T-Sequence such that
A7: ( dom Ls = O1 & ( for O2 being Ordinal st O2 in O1 holds
Ls . O2 = H1(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  S1[O1] by A2, A3, A7, Th17; ::_thesis: verum
end;
assume A8: a [= f . a ; ::_thesis: for O being Ordinal holds a [= (f,O) +. a
A9: now__::_thesis:_for_O1_being_Ordinal_st_S1[O1]_holds_
S1[_succ_O1]
let O1 be Ordinal; ::_thesis: ( S1[O1] implies S1[ succ O1] )
assume  S1[O1] ; ::_thesis: S1[ succ O1]
then  f . a [= f . ((f,O1) +. a) by QUANTAL1:def_12;
then  a [= f . ((f,O1) +. a) by A8, LATTICES:7;
hence  S1[ succ O1] by Th15; ::_thesis: verum
end;
A10: S1[ {} ] by Th13;
thus  for O being Ordinal holds S1[O] from ORDINAL2:sch_1(A10, A9, A1); ::_thesis: verum
end;

theorem Th23: :: KNASTER:23
for L being complete Lattice
for f being monotone UnOp of L
for a being Element of L st f . a [= a holds
for O being Ordinal holds (f,O) -. a [= a
proof
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 O being Ordinal holds (f,O) -. a [= a
let f be monotone UnOp of L; ::_thesis: for a being Element of L st f . a [= a holds
for O being Ordinal holds (f,O) -. a [= a
let a be Element of L; ::_thesis: ( f . a [= a implies for O being Ordinal holds (f,O) -. a [= a )
defpred S1[ Ordinal] means (f,$1) -. a [= a;
deffunc H1( Ordinal) ->  Element of L = (f,$1) -. a;
A1: now__::_thesis:_for_O1_being_Ordinal_st_O1_<>_{}_&_O1_is_limit_ordinal_&_(_for_O2_being_Ordinal_st_O2_in_O1_holds_
S1[O2]_)_holds_
S1[O1]
let O1 be Ordinal; ::_thesis: ( O1 <> {} & O1 is limit_ordinal & ( for O2 being Ordinal st O2 in O1 holds
S1[O2] ) implies S1[O1] )
assume that
A2: O1 <> {} and
A3: O1 is limit_ordinal and
A4: for O2 being Ordinal st O2 in O1 holds
S1[O2] ; ::_thesis: S1[O1]
consider O2 being set  such that
A5: O2 in O1 by A2, XBOOLE_0:def_1;
reconsider O2 = O2 as Ordinal by A5;
A6: S1[O2] by A4, A5;
consider Ls being T-Sequence such that
A7: ( dom Ls = O1 & ( for O2 being Ordinal st O2 in O1 holds
Ls . O2 = H1(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  S1[O1] by A2, A3, A7, Th18; ::_thesis: verum
end;
assume A8: f . a [= a ; ::_thesis: for O being Ordinal holds (f,O) -. a [= a
A9: now__::_thesis:_for_O1_being_Ordinal_st_S1[O1]_holds_
S1[_succ_O1]
let O1 be Ordinal; ::_thesis: ( S1[O1] implies S1[ succ O1] )
assume  S1[O1] ; ::_thesis: S1[ succ O1]
then  f . ((f,O1) -. a) [= f . a by QUANTAL1:def_12;
then  f . ((f,O1) -. a) [= a by A8, LATTICES:7;
hence  S1[ succ O1] by Th16; ::_thesis: verum
end;
A10: S1[ {} ] by Th14;
thus  for O being Ordinal holds S1[O] from ORDINAL2:sch_1(A10, A9, A1); ::_thesis: verum
end;

theorem Th24: :: KNASTER:24
for L being complete Lattice
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 holds
(f,O1) +. a [= (f,O2) +. a
proof
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 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 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 holds
(f,O1) +. a [= (f,O2) +. a )
defpred S1[ Ordinal] means  for O1, O2 being Ordinal st O1 c= O2 & O2 c= $1 holds
(f,O1) +. a [= (f,O2) +. a;
A1: now__::_thesis:_for_O4_being_Ordinal_st_O4_<>_{}_&_O4_is_limit_ordinal_&_(_for_O3_being_Ordinal_st_O3_in_O4_holds_
S1[O3]_)_holds_
S1[O4]
let O4 be Ordinal; ::_thesis: ( O4 <> {} & O4 is limit_ordinal & ( for O3 being Ordinal st O3 in O4 holds
S1[O3] ) implies S1[O4] )
assume that
A2: ( O4 <> {} & O4 is limit_ordinal ) and
A3: for O3 being Ordinal st O3 in O4 holds
S1[O3] ; ::_thesis: S1[O4]
thus  S1[O4] ::_thesis: verum
proof
let O1, O2 be Ordinal; ::_thesis: ( O1 c= O2 & O2 c= O4 implies (f,O1) +. a [= (f,O2) +. a )
assume that
A4: O1 c= O2 and
A5: O2 c= O4 ; ::_thesis: (f,O1) +. a [= (f,O2) +. a
A6: ( O2 c< O4 iff ( O2 c= O4 & O2 <> O4 ) ) by XBOOLE_0:def_8;
A7: ( O1 c< O2 iff ( O1 c= O2 & O1 <> O2 ) ) by XBOOLE_0:def_8;
percases ( O2 = O4 or O2 in O4 ) by A5, A6, ORDINAL1:11;
supposeA8: O2 = O4 ; ::_thesis: (f,O1) +. a [= (f,O2) +. a
thus  (f,O1) +. a [= (f,O2) +. a ::_thesis: verum
proof
percases ( O1 = O2 or O1 in O2 ) by A4, A7, ORDINAL1:11;
suppose O1 = O2 ; ::_thesis: (f,O1) +. a [= (f,O2) +. a
hence  (f,O1) +. a [= (f,O2) +. a ; ::_thesis: verum
end;
supposeA9: O1 in O2 ; ::_thesis: (f,O1) +. a [= (f,O2) +. a
deffunc H1( Ordinal) ->  Element of L = (f,$1) +. a;
consider L1 being T-Sequence such that
A10: ( dom L1 = O2 & ( for O3 being Ordinal st O3 in O2 holds
L1 . O3 = H1(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  (f,O1) +. a [= (f,O2) +. a by A11, LATTICE3:38; ::_thesis: verum
end;
end;
end;
end;
suppose O2 in O4 ; ::_thesis: (f,O1) +. a [= (f,O2) +. a
hence  (f,O1) +. a [= (f,O2) +. a by A3, A4; ::_thesis: verum
end;
end;
end;
end;
assume A12: a [= f . a ; ::_thesis: for O1, O2 being Ordinal st O1 c= O2 holds
(f,O1) +. a [= (f,O2) +. a
A13: now__::_thesis:_for_O4_being_Ordinal_st_S1[O4]_holds_
S1[_succ_O4]
let O4 be Ordinal; ::_thesis: ( S1[O4] implies S1[ succ O4] )
assume A14: S1[O4] ; ::_thesis: S1[ succ O4]
thus  S1[ succ O4] ::_thesis: verum
proof
let O1, O2 be Ordinal; ::_thesis: ( O1 c= O2 & O2 c= succ O4 implies (f,O1) +. a [= (f,O2) +. a )
assume that
A15: O1 c= O2 and
A16: O2 c= succ O4 ; ::_thesis: (f,O1) +. a [= (f,O2) +. a
percases ( ( O1 = O2 & O2 <> succ O4 ) or ( O1 <> O2 & O2 <> succ O4 ) or ( O1 = O2 & O2 = succ O4 ) or ( O1 <> O2 & O2 = succ O4 ) ) ;
suppose ( O1 = O2 & O2 <> succ O4 ) ; ::_thesis: (f,O1) +. a [= (f,O2) +. a
hence  (f,O1) +. a [= (f,O2) +. a ; ::_thesis: verum
end;
suppose ( O1 <> O2 & O2 <> succ O4 ) ; ::_thesis: (f,O1) +. a [= (f,O2) +. a
then  O2 c< succ O4 by A16, XBOOLE_0:def_8;
then  O2 in succ O4 by ORDINAL1:11;
then  O2 c= O4 by ORDINAL1:22;
hence  (f,O1) +. a [= (f,O2) +. a by A14, A15; ::_thesis: verum
end;
suppose ( O1 = O2 & O2 = succ O4 ) ; ::_thesis: (f,O1) +. a [= (f,O2) +. a
hence  (f,O1) +. a [= (f,O2) +. a ; ::_thesis: verum
end;
supposeA17: ( O1 <> O2 & O2 = succ O4 ) ; ::_thesis: (f,O1) +. a [= (f,O2) +. a
A18: (f,O4) +. a [= (f,(succ O4)) +. a
proof
percases ( O4 is limit_ordinal or ex O3 being Ordinal st O4 = succ O3 ) by ORDINAL1:29;
supposeA19: O4 is limit_ordinal ; ::_thesis: (f,O4) +. a [= (f,(succ O4)) +. a
thus  (f,O4) +. a [= (f,(succ O4)) +. a ::_thesis: verum
proof
percases ( O4 = {} or O4 <> {} ) ;
suppose O4 = {} ; ::_thesis: (f,O4) +. a [= (f,(succ O4)) +. a
then  (f,O4) +. a = a by Th13;
hence  (f,O4) +. a [= (f,(succ O4)) +. a by A12, Th15; ::_thesis: verum
end;
supposeA20: O4 <> {} ; ::_thesis: (f,O4) +. a [= (f,(succ O4)) +. a
deffunc H1( Ordinal) ->  Element of L = (f,$1) +. a;
consider L1 being T-Sequence such that
A21: ( dom L1 = O4 & ( for O3 being Ordinal st O3 in O4 holds
L1 . O3 = H1(O3) ) ) from ORDINAL2:sch_2();
A22: rng L1 is_less_than (f,(succ O4)) +. a
proof
let q be Element of L; :: according to LATTICE3:def_17 ::_thesis: ( not q in rng L1 or q [= (f,(succ O4)) +. a )
assume  q in rng L1 ; ::_thesis: q [= (f,(succ O4)) +. a
then consider O3 being set  such that
A23: O3 in dom L1 and
A24: q = L1 . O3 by FUNCT_1:def_3;
reconsider O3 = 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; ::_thesis: verum
end;
 (f,O4) +. a = "\/" ((rng L1),L) by A19, A20, A21, Th17;
hence  (f,O4) +. a [= (f,(succ O4)) +. a by A22, LATTICE3:def_21; ::_thesis: verum
end;
end;
end;
end;
suppose ex O3 being Ordinal st O4 = succ O3 ; ::_thesis: (f,O4) +. a [= (f,(succ O4)) +. a
then consider O3 being Ordinal such that
A28: O4 = succ O3 ;
 succ O3 = O3 \/ {O3} by ORDINAL1:def_1;
then  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  (f,O4) +. a [= (f,(succ O4)) +. a by Th15; ::_thesis: verum
end;
end;
end;
 O1 c< O2 by A15, A17, XBOOLE_0:def_8;
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  (f,O1) +. a [= (f,O2) +. a by A17, A18, LATTICES:7; ::_thesis: verum
end;
end;
end;
end;
let O1, O2 be Ordinal; ::_thesis: ( O1 c= O2 implies (f,O1) +. a [= (f,O2) +. a )
assume A29: O1 c= O2 ; ::_thesis: (f,O1) +. a [= (f,O2) +. a
A30: S1[ {} ] ;
 for O4 being Ordinal holds S1[O4] from ORDINAL2:sch_1(A30, A13, A1);
hence  (f,O1) +. a [= (f,O2) +. a by A29; ::_thesis: verum
end;

theorem Th25: :: KNASTER:25
for L being 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 holds
(f,O2) -. a [= (f,O1) -. a
proof
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 holds
(f,O2) -. a [= (f,O1) -. 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 holds
(f,O2) -. a [= (f,O1) -. a
let a be Element of L; ::_thesis: ( f . a [= a implies for O1, O2 being Ordinal st O1 c= O2 holds
(f,O2) -. a [= (f,O1) -. a )
defpred S1[ Ordinal] means  for O1, O2 being Ordinal st O1 c= O2 & O2 c= $1 holds
(f,O2) -. a [= (f,O1) -. a;
A1: now__::_thesis:_for_O4_being_Ordinal_st_O4_<>_{}_&_O4_is_limit_ordinal_&_(_for_O3_being_Ordinal_st_O3_in_O4_holds_
S1[O3]_)_holds_
S1[O4]
let O4 be Ordinal; ::_thesis: ( O4 <> {} & O4 is limit_ordinal & ( for O3 being Ordinal st O3 in O4 holds
S1[O3] ) implies S1[O4] )
assume that
A2: ( O4 <> {} & O4 is limit_ordinal ) and
A3: for O3 being Ordinal st O3 in O4 holds
S1[O3] ; ::_thesis: S1[O4]
thus  S1[O4] ::_thesis: verum
proof
let O1, O2 be Ordinal; ::_thesis: ( O1 c= O2 & O2 c= O4 implies (f,O2) -. a [= (f,O1) -. a )
assume that
A4: O1 c= O2 and
A5: O2 c= O4 ; ::_thesis: (f,O2) -. a [= (f,O1) -. a
A6: ( O2 c< O4 iff ( O2 c= O4 & O2 <> O4 ) ) by XBOOLE_0:def_8;
A7: ( O1 c< O2 iff ( O1 c= O2 & O1 <> O2 ) ) by XBOOLE_0:def_8;
percases ( O2 = O4 or O2 in O4 ) by A5, A6, ORDINAL1:11;
supposeA8: O2 = O4 ; ::_thesis: (f,O2) -. a [= (f,O1) -. a
thus  (f,O2) -. a [= (f,O1) -. a ::_thesis: verum
proof
percases ( O1 = O2 or O1 in O2 ) by A4, A7, ORDINAL1:11;
suppose O1 = O2 ; ::_thesis: (f,O2) -. a [= (f,O1) -. a
hence  (f,O2) -. a [= (f,O1) -. a ; ::_thesis: verum
end;
supposeA9: O1 in O2 ; ::_thesis: (f,O2) -. a [= (f,O1) -. a
deffunc H1( Ordinal) ->  Element of L = (f,$1) -. a;
consider L1 being T-Sequence such that
A10: ( dom L1 = O2 & ( for O3 being Ordinal st O3 in O2 holds
L1 . O3 = H1(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  (f,O2) -. a [= (f,O1) -. a by A11, LATTICE3:38; ::_thesis: verum
end;
end;
end;
end;
suppose O2 in O4 ; ::_thesis: (f,O2) -. a [= (f,O1) -. a
hence  (f,O2) -. a [= (f,O1) -. a by A3, A4; ::_thesis: verum
end;
end;
end;
end;
assume A12: f . a [= a ; ::_thesis: for O1, O2 being Ordinal st O1 c= O2 holds
(f,O2) -. a [= (f,O1) -. a
A13: now__::_thesis:_for_O4_being_Ordinal_st_S1[O4]_holds_
S1[_succ_O4]
let O4 be Ordinal; ::_thesis: ( S1[O4] implies S1[ succ O4] )
assume A14: S1[O4] ; ::_thesis: S1[ succ O4]
thus  S1[ succ O4] ::_thesis: verum
proof
let O1, O2 be Ordinal; ::_thesis: ( O1 c= O2 & O2 c= succ O4 implies (f,O2) -. a [= (f,O1) -. a )
assume that
A15: O1 c= O2 and
A16: O2 c= succ O4 ; ::_thesis: (f,O2) -. a [= (f,O1) -. a
percases ( ( O1 = O2 & O2 <> succ O4 ) or ( O1 <> O2 & O2 <> succ O4 ) or ( O1 = O2 & O2 = succ O4 ) or ( O1 <> O2 & O2 = succ O4 ) ) ;
suppose ( O1 = O2 & O2 <> succ O4 ) ; ::_thesis: (f,O2) -. a [= (f,O1) -. a
hence  (f,O2) -. a [= (f,O1) -. a ; ::_thesis: verum
end;
suppose ( O1 <> O2 & O2 <> succ O4 ) ; ::_thesis: (f,O2) -. a [= (f,O1) -. a
then  O2 c< succ O4 by A16, XBOOLE_0:def_8;
then  O2 in succ O4 by ORDINAL1:11;
then  O2 c= O4 by ORDINAL1:22;
hence  (f,O2) -. a [= (f,O1) -. a by A14, A15; ::_thesis: verum
end;
suppose ( O1 = O2 & O2 = succ O4 ) ; ::_thesis: (f,O2) -. a [= (f,O1) -. a
hence  (f,O2) -. a [= (f,O1) -. a ; ::_thesis: verum
end;
supposeA17: ( O1 <> O2 & O2 = succ O4 ) ; ::_thesis: (f,O2) -. a [= (f,O1) -. a
A18: (f,(succ O4)) -. a [= (f,O4) -. a
proof
percases ( O4 is limit_ordinal or ex O3 being Ordinal st O4 = succ O3 ) by ORDINAL1:29;
supposeA19: O4 is limit_ordinal ; ::_thesis: (f,(succ O4)) -. a [= (f,O4) -. a
thus  (f,(succ O4)) -. a [= (f,O4) -. a ::_thesis: verum
proof
percases ( O4 = {} or O4 <> {} ) ;
suppose O4 = {} ; ::_thesis: (f,(succ O4)) -. a [= (f,O4) -. a
then  (f,O4) -. a = a by Th14;
hence  (f,(succ O4)) -. a [= (f,O4) -. a by A12, Th16; ::_thesis: verum
end;
supposeA20: O4 <> {} ; ::_thesis: (f,(succ O4)) -. a [= (f,O4) -. a
deffunc H1( Ordinal) ->  Element of L = (f,$1) -. a;
consider L1 being T-Sequence such that
A21: ( dom L1 = O4 & ( for O3 being Ordinal st O3 in O4 holds
L1 . O3 = H1(O3) ) ) from ORDINAL2:sch_2();
A22: (f,(succ O4)) -. a is_less_than rng L1
proof
let q be Element of L; :: according to LATTICE3:def_16 ::_thesis: ( not q in rng L1 or (f,(succ O4)) -. a [= q )
assume  q in rng L1 ; ::_thesis: (f,(succ O4)) -. a [= q
then consider O3 being set  such that
A23: O3 in dom L1 and
A24: q = L1 . O3 by FUNCT_1:def_3;
reconsider O3 = 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; ::_thesis: verum
end;
 (f,O4) -. a = "/\" ((rng L1),L) by A19, A20, A21, Th18;
hence  (f,(succ O4)) -. a [= (f,O4) -. a by A22, LATTICE3:34; ::_thesis: verum
end;
end;
end;
end;
suppose ex O3 being Ordinal st O4 = succ O3 ; ::_thesis: (f,(succ O4)) -. a [= (f,O4) -. a
then consider O3 being Ordinal such that
A28: O4 = succ O3 ;
 succ O3 = O3 \/ {O3} by ORDINAL1:def_1;
then  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  (f,(succ O4)) -. a [= (f,O4) -. a by Th16; ::_thesis: verum
end;
end;
end;
 O1 c< O2 by A15, A17, XBOOLE_0:def_8;
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  (f,O2) -. a [= (f,O1) -. a by A17, A18, LATTICES:7; ::_thesis: verum
end;
end;
end;
end;
let O1, O2 be Ordinal; ::_thesis: ( O1 c= O2 implies (f,O2) -. a [= (f,O1) -. a )
assume A29: O1 c= O2 ; ::_thesis: (f,O2) -. a [= (f,O1) -. a
A30: S1[ {} ] ;
 for O4 being Ordinal holds S1[O4] from ORDINAL2:sch_1(A30, A13, A1);
hence  (f,O2) -. a [= (f,O1) -. a by A29; ::_thesis: verum
end;

theorem Th26: :: KNASTER:26
for L being complete Lattice
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
proof
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 )
 succ O1 = O1 \/ {O1} by ORDINAL1:def_1;
then 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, ABIAN:def_4; ::_thesis: verum
end;

theorem Th27: :: KNASTER:27
for L being 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
proof
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, 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, ABIAN:def_4; ::_thesis: verum
end;

theorem Th28: :: KNASTER:28
for O1 being Ordinal
for L being complete Lattice
for f being monotone UnOp of L
for a being Element of L st a [= f . a & (f,O1) +. a is_a_fixpoint_of f holds
for O2 being Ordinal st O1 c= O2 holds
(f,O1) +. a = (f,O2) +. a
proof
let O1 be Ordinal; ::_thesis: for L being complete Lattice
for f being monotone UnOp of L
for a being Element of L st a [= f . a & (f,O1) +. a is_a_fixpoint_of f holds
for O2 being Ordinal st O1 c= O2 holds
(f,O1) +. a = (f,O2) +. a
let L be complete Lattice; ::_thesis: for f being monotone UnOp of L
for a being Element of L st a [= f . a & (f,O1) +. a is_a_fixpoint_of f holds
for O2 being Ordinal st O1 c= O2 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 & (f,O1) +. a is_a_fixpoint_of f holds
for O2 being Ordinal st O1 c= O2 holds
(f,O1) +. a = (f,O2) +. a
let a be Element of L; ::_thesis: ( a [= f . a & (f,O1) +. a is_a_fixpoint_of f implies for O2 being Ordinal st O1 c= O2 holds
(f,O1) +. a = (f,O2) +. a )
assume that
A1: a [= f . a and
A2: (f,O1) +. a is_a_fixpoint_of f ; ::_thesis: for O2 being Ordinal st O1 c= O2 holds
(f,O1) +. a = (f,O2) +. a
set fa = (f,O1) +. a;
defpred S1[ Ordinal] means ( O1 c= $1 implies (f,O1) +. a = (f,$1) +. a );
A3: now__::_thesis:_for_O2_being_Ordinal_st_O2_<>_{}_&_O2_is_limit_ordinal_&_(_for_O3_being_Ordinal_st_O3_in_O2_holds_
S1[O3]_)_holds_
S1[O2]
let O2 be Ordinal; ::_thesis: ( O2 <> {} & O2 is limit_ordinal & ( for O3 being Ordinal st O3 in O2 holds
S1[O3] ) implies S1[O2] )
assume that
A4: ( O2 <> {} & O2 is limit_ordinal ) and
A5: for O3 being Ordinal st O3 in O2 holds
S1[O3] ; ::_thesis: S1[O2]
thus  S1[O2] ::_thesis: verum
proof
assume  O1 c= O2 ; ::_thesis: (f,O1) +. a = (f,O2) +. a
then A6: (f,O1) +. a [= (f,O2) +. a by A1, Th24;
deffunc H1( Ordinal) ->  Element of L = (f,$1) +. a;
consider L1 being T-Sequence such that
A7: ( dom L1 = O2 & ( for O3 being Ordinal st O3 in O2 holds
L1 . O3 = H1(O3) ) ) from ORDINAL2:sch_2();
A8: rng L1 is_less_than (f,O1) +. a
proof
let q be Element of L; :: according to LATTICE3:def_17 ::_thesis: ( not q in rng L1 or q [= (f,O1) +. a )
assume  q in rng L1 ; ::_thesis: q [= (f,O1) +. a
then consider O3 being set  such that
A9: O3 in dom L1 and
A10: q = L1 . O3 by FUNCT_1:def_3;
reconsider O3 = O3 as Ordinal by A9;
percases ( O1 c= O3 or O3 c= O1 ) ;
suppose O1 c= O3 ; ::_thesis: q [= (f,O1) +. a
then  (f,O3) +. a [= (f,O1) +. a by A5, A7, A9;
hence  q [= (f,O1) +. a by A7, A9, A10; ::_thesis: verum
end;
suppose O3 c= O1 ; ::_thesis: q [= (f,O1) +. a
then  (f,O3) +. a [= (f,O1) +. a by A1, Th24;
hence  q [= (f,O1) +. a by A7, A9, A10; ::_thesis: verum
end;
end;
end;
 (f,O2) +. a = "\/" ((rng L1),L) by A4, A7, Th17;
then  (f,O2) +. a [= (f,O1) +. a by A8, LATTICE3:def_21;
hence  (f,O1) +. a = (f,O2) +. a by A6, LATTICES:8; ::_thesis: verum
end;
end;
A11: now__::_thesis:_for_O2_being_Ordinal_st_S1[O2]_holds_
S1[_succ_O2]
let O2 be Ordinal; ::_thesis: ( S1[O2] implies S1[ succ O2] )
assume A12: S1[O2] ; ::_thesis: S1[ succ O2]
thus  S1[ succ O2] ::_thesis: verum
proof
assume A13: O1 c= succ O2 ; ::_thesis: (f,O1) +. a = (f,(succ O2)) +. a
percases ( O1 = succ O2 or O1 <> succ O2 ) ;
suppose O1 = succ O2 ; ::_thesis: (f,O1) +. a = (f,(succ O2)) +. a
hence  (f,O1) +. a = (f,(succ O2)) +. a ; ::_thesis: verum
end;
suppose O1 <> succ O2 ; ::_thesis: (f,O1) +. a = (f,(succ O2)) +. a
then  O1 c< succ O2 by A13, XBOOLE_0:def_8;
then  O1 in succ O2 by ORDINAL1:11;
hence (f,O1) +. a = f . ((f,O2) +. a) by A2, A12, ABIAN:def_3, ORDINAL1:22
.= (f,(succ O2)) +. a by Th15 ;
::_thesis: verum
end;
end;
end;
end;
A14: S1[ {} ] ;
thus  for O2 being Ordinal holds S1[O2] from ORDINAL2:sch_1(A14, A11, A3); ::_thesis: verum
end;

theorem Th29: :: KNASTER:29
for O1 being Ordinal
for L being complete Lattice
for f being monotone UnOp of L
for a being Element of L st f . a [= a & (f,O1) -. a is_a_fixpoint_of f holds
for O2 being Ordinal st O1 c= O2 holds
(f,O1) -. a = (f,O2) -. a
proof
let O1 be Ordinal; ::_thesis: for L being complete Lattice
for f being monotone UnOp of L
for a being Element of L st f . a [= a & (f,O1) -. a is_a_fixpoint_of f holds
for O2 being Ordinal st O1 c= O2 holds
(f,O1) -. a = (f,O2) -. a
let L be complete Lattice; ::_thesis: for f being monotone UnOp of L
for a being Element of L st f . a [= a & (f,O1) -. a is_a_fixpoint_of f holds
for O2 being Ordinal st O1 c= O2 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 & (f,O1) -. a is_a_fixpoint_of f holds
for O2 being Ordinal st O1 c= O2 holds
(f,O1) -. a = (f,O2) -. a
let a be Element of L; ::_thesis: ( f . a [= a & (f,O1) -. a is_a_fixpoint_of f implies for O2 being Ordinal st O1 c= O2 holds
(f,O1) -. a = (f,O2) -. a )
assume that
A1: f . a [= a and
A2: (f,O1) -. a is_a_fixpoint_of f ; ::_thesis: for O2 being Ordinal st O1 c= O2 holds
(f,O1) -. a = (f,O2) -. a
set fa = (f,O1) -. a;
defpred S1[ Ordinal] means ( O1 c= $1 implies (f,O1) -. a = (f,$1) -. a );
A3: now__::_thesis:_for_O2_being_Ordinal_st_O2_<>_{}_&_O2_is_limit_ordinal_&_(_for_O3_being_Ordinal_st_O3_in_O2_holds_
S1[O3]_)_holds_
S1[O2]
let O2 be Ordinal; ::_thesis: ( O2 <> {} & O2 is limit_ordinal & ( for O3 being Ordinal st O3 in O2 holds
S1[O3] ) implies S1[O2] )
assume that
A4: ( O2 <> {} & O2 is limit_ordinal ) and
A5: for O3 being Ordinal st O3 in O2 holds
S1[O3] ; ::_thesis: S1[O2]
thus  S1[O2] ::_thesis: verum
proof
assume  O1 c= O2 ; ::_thesis: (f,O1) -. a = (f,O2) -. a
then A6: (f,O2) -. a [= (f,O1) -. a by A1, Th25;
deffunc H1( Ordinal) ->  Element of L = (f,$1) -. a;
consider L1 being T-Sequence such that
A7: ( dom L1 = O2 & ( for O3 being Ordinal st O3 in O2 holds
L1 . O3 = H1(O3) ) ) from ORDINAL2:sch_2();
A8: (f,O1) -. a is_less_than rng L1
proof
let q be Element of L; :: according to LATTICE3:def_16 ::_thesis: ( not q in rng L1 or (f,O1) -. a [= q )
assume  q in rng L1 ; ::_thesis: (f,O1) -. a [= q
then consider O3 being set  such that
A9: O3 in dom L1 and
A10: q = L1 . O3 by FUNCT_1:def_3;
reconsider O3 = O3 as Ordinal by A9;
percases ( O1 c= O3 or O3 c= O1 ) ;
suppose O1 c= O3 ; ::_thesis: (f,O1) -. a [= q
then  (f,O1) -. a [= (f,O3) -. a by A5, A7, A9;
hence  (f,O1) -. a [= q by A7, A9, A10; ::_thesis: verum
end;
suppose O3 c= O1 ; ::_thesis: (f,O1) -. a [= q
then  (f,O1) -. a [= (f,O3) -. a by A1, Th25;
hence  (f,O1) -. a [= q by A7, A9, A10; ::_thesis: verum
end;
end;
end;
 (f,O2) -. a = "/\" ((rng L1),L) by A4, A7, Th18;
then  (f,O1) -. a [= (f,O2) -. a by A8, LATTICE3:39;
hence  (f,O1) -. a = (f,O2) -. a by A6, LATTICES:8; ::_thesis: verum
end;
end;
A11: now__::_thesis:_for_O2_being_Ordinal_st_S1[O2]_holds_
S1[_succ_O2]
let O2 be Ordinal; ::_thesis: ( S1[O2] implies S1[ succ O2] )
assume A12: S1[O2] ; ::_thesis: S1[ succ O2]
thus  S1[ succ O2] ::_thesis: verum
proof
assume A13: O1 c= succ O2 ; ::_thesis: (f,O1) -. a = (f,(succ O2)) -. a
percases ( O1 = succ O2 or O1 <> succ O2 ) ;
suppose O1 = succ O2 ; ::_thesis: (f,O1) -. a = (f,(succ O2)) -. a
hence  (f,O1) -. a = (f,(succ O2)) -. a ; ::_thesis: verum
end;
suppose O1 <> succ O2 ; ::_thesis: (f,O1) -. a = (f,(succ O2)) -. a
then  O1 c< succ O2 by A13, XBOOLE_0:def_8;
then  O1 in succ O2 by ORDINAL1:11;
hence (f,O1) -. a = f . ((f,O2) -. a) by A2, A12, ABIAN:def_3, ORDINAL1:22
.= (f,(succ O2)) -. a by Th16 ;
::_thesis: verum
end;
end;
end;
end;
A14: S1[ {} ] ;
thus  for O2 being Ordinal holds S1[O2] from ORDINAL2:sch_1(A14, A11, A3); ::_thesis: verum
end;

Lm1:  for O1, O2 being Ordinal holds
( O1 c< O2 or O1 = O2 or O2 c< O1 )
proof
let O1, O2 be Ordinal; ::_thesis: ( O1 c< O2 or O1 = O2 or O2 c< O1 )
assume that
A1: ( not O1 c< O2 & not O1 = O2 ) and
A2: not O2 c< O1 ; ::_thesis: contradiction
 not O1 c= O2 by A1, XBOOLE_0:def_8;
hence  contradiction by A2, XBOOLE_0:def_8; ::_thesis: verum
end;

theorem Th30: :: KNASTER:30
for L being complete Lattice
for f being monotone UnOp of L
for a being Element of L st a [= f . a holds
ex O being Ordinal st
( card O c= card the carrier of L & (f,O) +. a is_a_fixpoint_of f )
proof
let L be complete Lattice; ::_thesis: for f being monotone UnOp of L
for a being Element of L st a [= f . a holds
ex O being Ordinal st
( card O c= card the carrier of L & (f,O) +. a is_a_fixpoint_of f )
let f be monotone UnOp of L; ::_thesis: for a being Element of L st a [= f . a holds
ex O being Ordinal st
( card O c= card the carrier of L & (f,O) +. a is_a_fixpoint_of f )
let a be Element of L; ::_thesis: ( a [= f . a implies ex O being Ordinal st
( card O c= card the carrier of L & (f,O) +. a is_a_fixpoint_of f ) )
set cL = the carrier of L;
set ccL = card the carrier of L;
set nccL = nextcard (card the carrier of L);
deffunc H1( Ordinal) ->  Element of L = (f,$1) +. a;
consider Ls being T-Sequence such that
A1: ( dom Ls = nextcard (card the carrier of L) & ( for O2 being Ordinal st O2 in nextcard (card the carrier of L) holds
Ls . O2 = H1(O2) ) ) from ORDINAL2:sch_2();
assume A2: a [= f . a ; ::_thesis: ex O being Ordinal st
( card O c= card the carrier of L & (f,O) +. a is_a_fixpoint_of f )
now__::_thesis:_ex_O_being_Ordinal_st_
(_O_in_nextcard_(card_the_carrier_of_L)_&_(f,O)_+._a_is_a_fixpoint_of_f_)
assume A3: for O being Ordinal st O in nextcard (card the carrier of L) holds
not (f,O) +. a is_a_fixpoint_of f ; ::_thesis: contradiction
A4: Ls is one-to-one
proof
let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom Ls or not x2 in dom Ls or not Ls . x1 = Ls . x2 or x1 = x2 )
assume that
A5: x1 in dom Ls and
A6: x2 in dom Ls and
A7: Ls . x1 = Ls . x2 ; ::_thesis: x1 = x2
reconsider x1 = x1, x2 = x2 as Ordinal by A5, A6;
A8: Ls . x1 = (f,x1) +. a by A1, A5;
A9: Ls . x2 = (f,x2) +. a by A1, A6;
percases ( x1 c< x2 or x2 c< x1 or x2 = x1 ) by Lm1;
supposeA10: x1 c< x2 ; ::_thesis: x1 = x2
 not (f,x2) +. a is_a_fixpoint_of f by A1, A3, A6;
hence  x1 = x2 by A2, A1, A6, A7, A8, A10, Th26; ::_thesis: verum
end;
supposeA11: x2 c< x1 ; ::_thesis: x1 = x2
 not (f,x1) +. a is_a_fixpoint_of f by A1, A3, A5;
hence  x1 = x2 by A2, A1, A5, A7, A9, A11, Th26; ::_thesis: verum
end;
suppose x2 = x1 ; ::_thesis: x1 = x2
hence  x1 = x2 ; ::_thesis: verum
end;
end;
end;
 rng Ls c= the carrier of L
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng Ls or y in the carrier of L )
assume  y in rng Ls ; ::_thesis: y in the carrier of L
then consider x being set  such that
A12: x in dom Ls and
A13: Ls . x = y by FUNCT_1:def_3;
reconsider x = x as Ordinal by A12;
 Ls . x = (f,x) +. a by A1, A12;
hence  y in the carrier of L by A13; ::_thesis: verum
end;
then  card (nextcard (card the carrier of L)) c= card the carrier of L by A1, A4, CARD_1:10;
then A14: nextcard (card the carrier of L) c= card the carrier of L by CARD_1:def_2;
 card the carrier of L in nextcard (card the carrier of L) by CARD_1:18;
hence  contradiction by A14, CARD_1:4; ::_thesis: verum
end;
then consider O being Ordinal such that
A15: O in nextcard (card the carrier of L) and
A16: (f,O) +. a is_a_fixpoint_of f ;
take  O ; ::_thesis: ( card O c= card the carrier of L & (f,O) +. a is_a_fixpoint_of f )
 card O in nextcard (card the carrier of L) by A15, CARD_1:9;
hence  card O c= card the carrier of L by CARD_3:91; ::_thesis: (f,O) +. a is_a_fixpoint_of f
thus  (f,O) +. a is_a_fixpoint_of f by A16; ::_thesis: verum
end;

theorem Th31: :: KNASTER:31
for L being complete Lattice
for f being monotone UnOp of L
for a being Element of L st f . a [= a holds
ex O being Ordinal st
( card O c= card the carrier of L & (f,O) -. a is_a_fixpoint_of f )
proof
let L be complete Lattice; ::_thesis: for f being monotone UnOp of L
for a being Element of L st f . a [= a holds
ex O being Ordinal st
( card O c= card the carrier of L & (f,O) -. a is_a_fixpoint_of f )
let f be monotone UnOp of L; ::_thesis: for a being Element of L st f . a [= a holds
ex O being Ordinal st
( card O c= card the carrier of L & (f,O) -. a is_a_fixpoint_of f )
let a be Element of L; ::_thesis: ( f . a [= a implies ex O being Ordinal st
( card O c= card the carrier of L & (f,O) -. a is_a_fixpoint_of f ) )
set cL = the carrier of L;
set ccL = card the carrier of L;
set nccL = nextcard (card the carrier of L);
deffunc H1( Ordinal) ->  Element of L = (f,$1) -. a;
consider Ls being T-Sequence such that
A1: ( dom Ls = nextcard (card the carrier of L) & ( for O2 being Ordinal st O2 in nextcard (card the carrier of L) holds
Ls . O2 = H1(O2) ) ) from ORDINAL2:sch_2();
assume A2: f . a [= a ; ::_thesis: ex O being Ordinal st
( card O c= card the carrier of L & (f,O) -. a is_a_fixpoint_of f )
now__::_thesis:_ex_O_being_Ordinal_st_
(_O_in_nextcard_(card_the_carrier_of_L)_&_(f,O)_-._a_is_a_fixpoint_of_f_)
assume A3: for O being Ordinal st O in nextcard (card the carrier of L) holds
not (f,O) -. a is_a_fixpoint_of f ; ::_thesis: contradiction
A4: Ls is one-to-one
proof
let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom Ls or not x2 in dom Ls or not Ls . x1 = Ls . x2 or x1 = x2 )
assume that
A5: x1 in dom Ls and
A6: x2 in dom Ls and
A7: Ls . x1 = Ls . x2 ; ::_thesis: x1 = x2
reconsider x1 = x1, x2 = x2 as Ordinal by A5, A6;
A8: Ls . x1 = (f,x1) -. a by A1, A5;
A9: Ls . x2 = (f,x2) -. a by A1, A6;
percases ( x1 c< x2 or x2 c< x1 or x2 = x1 ) by Lm1;
supposeA10: x1 c< x2 ; ::_thesis: x1 = x2
 not (f,x2) -. a is_a_fixpoint_of f by A1, A3, A6;
hence  x1 = x2 by A2, A1, A6, A7, A8, A10, Th27; ::_thesis: verum
end;
supposeA11: x2 c< x1 ; ::_thesis: x1 = x2
 not (f,x1) -. a is_a_fixpoint_of f by A1, A3, A5;
hence  x1 = x2 by A2, A1, A5, A7, A9, A11, Th27; ::_thesis: verum
end;
suppose x2 = x1 ; ::_thesis: x1 = x2
hence  x1 = x2 ; ::_thesis: verum
end;
end;
end;
 rng Ls c= the carrier of L
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng Ls or y in the carrier of L )
assume  y in rng Ls ; ::_thesis: y in the carrier of L
then consider x being set  such that
A12: x in dom Ls and
A13: Ls . x = y by FUNCT_1:def_3;
reconsider x = x as Ordinal by A12;
 Ls . x = (f,x) -. a by A1, A12;
hence  y in the carrier of L by A13; ::_thesis: verum
end;
then  card (nextcard (card the carrier of L)) c= card the carrier of L by A1, A4, CARD_1:10;
then A14: nextcard (card the carrier of L) c= card the carrier of L by CARD_1:def_2;
 card the carrier of L in nextcard (card the carrier of L) by CARD_1:18;
hence  contradiction by A14, CARD_1:4; ::_thesis: verum
end;
then consider O being Ordinal such that
A15: O in nextcard (card the carrier of L) and
A16: (f,O) -. a is_a_fixpoint_of f ;
take  O ; ::_thesis: ( card O c= card the carrier of L & (f,O) -. a is_a_fixpoint_of f )
 card O in nextcard (card the carrier of L) by A15, CARD_1:9;
hence  card O c= card the carrier of L by CARD_3:91; ::_thesis: (f,O) -. a is_a_fixpoint_of f
thus  (f,O) -. a is_a_fixpoint_of f by A16; ::_thesis: verum
end;

theorem Th32: :: KNASTER:32
for L being complete Lattice
for f being monotone UnOp of L
for a, b being Element of L st a is_a_fixpoint_of f & b is_a_fixpoint_of f holds
ex O being Ordinal 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 L be complete Lattice; ::_thesis: for f being monotone UnOp of L
for a, b being Element of L st a is_a_fixpoint_of f & b is_a_fixpoint_of f holds
ex O being Ordinal 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) )
let f be monotone UnOp of L; ::_thesis: for a, b being Element of L st a is_a_fixpoint_of f & b is_a_fixpoint_of f holds
ex O being Ordinal 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) )
let a, b be Element of L; ::_thesis: ( a is_a_fixpoint_of f & b is_a_fixpoint_of f implies ex O being Ordinal 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) ) )
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 ) ; ::_thesis: ex O being Ordinal 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) )
then A5: ( a = f . a & b = f . b ) by ABIAN:def_3;
then consider O being Ordinal 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 ; ::_thesis: ( 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) )
thus  ( card O c= card the carrier of L & (f,O) +. (a "\/" b) is_a_fixpoint_of f ) by A6; ::_thesis: ( a [= (f,O) +. (a "\/" b) & b [= (f,O) +. (a "\/" b) )
 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; ::_thesis: b [= (f,O) +. (a "\/" b)
thus  b [= (f,O) +. (a "\/" b) by A3, A7, LATTICES:7; ::_thesis: verum
end;

theorem Th33: :: KNASTER:33
for L being complete Lattice
for f being monotone UnOp of L
for a, b being Element of L st a is_a_fixpoint_of f & b is_a_fixpoint_of f holds
ex O being Ordinal 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 L be complete Lattice; ::_thesis: for f being monotone UnOp of L
for a, b being Element of L st a is_a_fixpoint_of f & b is_a_fixpoint_of f holds
ex O being Ordinal 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 )
let f be monotone UnOp of L; ::_thesis: for a, b being Element of L st a is_a_fixpoint_of f & b is_a_fixpoint_of f holds
ex O being Ordinal 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 )
let a, b be Element of L; ::_thesis: ( a is_a_fixpoint_of f & b is_a_fixpoint_of f implies ex O being Ordinal 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 ) )
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 ) ; ::_thesis: ex O being Ordinal 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 )
then A5: ( a = f . a & b = f . b ) by ABIAN:def_3;
then consider O being Ordinal 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 ; ::_thesis: ( 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 )
thus  ( card O c= card the carrier of L & (f,O) -. (a "/\" b) is_a_fixpoint_of f ) by A6; ::_thesis: ( (f,O) -. (a "/\" b) [= a & (f,O) -. (a "/\" b) [= b )
 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; ::_thesis: (f,O) -. (a "/\" b) [= b
thus  (f,O) -. (a "/\" b) [= b by A3, A7, LATTICES:7; ::_thesis: verum
end;

theorem Th34: :: KNASTER:34
for L being complete Lattice
for f being monotone UnOp of L
for a, b being Element of L st a [= b & b is_a_fixpoint_of f holds
for O2 being Ordinal holds (f,O2) +. a [= b
proof
let L be complete Lattice; ::_thesis: for f being monotone UnOp of L
for a, b being Element of L st a [= b & b is_a_fixpoint_of f holds
for O2 being Ordinal holds (f,O2) +. a [= b
let f be monotone UnOp of L; ::_thesis: for a, b being Element of L st a [= b & b is_a_fixpoint_of f holds
for O2 being Ordinal holds (f,O2) +. a [= b
let a, b be Element of L; ::_thesis: ( a [= b & b is_a_fixpoint_of f implies for O2 being Ordinal holds (f,O2) +. a [= b )
assume that
A1: a [= b and
A2: b is_a_fixpoint_of f ; ::_thesis: for O2 being Ordinal holds (f,O2) +. a [= b
defpred S1[ Ordinal] means (f,$1) +. a [= b;
A3: f . b = b by A2, ABIAN:def_3;
A4: now__::_thesis:_for_O1_being_Ordinal_st_S1[O1]_holds_
S1[_succ_O1]
let O1 be Ordinal; ::_thesis: ( S1[O1] implies S1[ succ O1] )
assume  S1[O1] ; ::_thesis: S1[ succ O1]
then  f . ((f,O1) +. a) [= f . b by QUANTAL1:def_12;
hence  S1[ succ O1] by A3, Th15; ::_thesis: verum
end;
A5: now__::_thesis:_for_O1_being_Ordinal_st_O1_<>_{}_&_O1_is_limit_ordinal_&_(_for_O2_being_Ordinal_st_O2_in_O1_holds_
S1[O2]_)_holds_
S1[O1]
deffunc H1( Ordinal) ->  Element of L = (f,$1) +. a;
let O1 be Ordinal; ::_thesis: ( O1 <> {} & O1 is limit_ordinal & ( for O2 being Ordinal st O2 in O1 holds
S1[O2] ) implies S1[O1] )
assume that
A6: ( O1 <> {} & O1 is limit_ordinal ) and
A7: for O2 being Ordinal st O2 in O1 holds
S1[O2] ; ::_thesis: S1[O1]
consider L1 being T-Sequence such that
A8: ( dom L1 = O1 & ( for O3 being Ordinal st O3 in O1 holds
L1 . O3 = H1(O3) ) ) from ORDINAL2:sch_2();
A9: rng L1 is_less_than b
proof
let q be Element of L; :: according to LATTICE3:def_17 ::_thesis: ( not q in rng L1 or q [= b )
assume  q in rng L1 ; ::_thesis: q [= b
then consider O3 being set  such that
A10: O3 in dom L1 and
A11: q = L1 . O3 by FUNCT_1:def_3;
reconsider O3 = O3 as Ordinal by A10;
 (f,O3) +. a [= b by A7, A8, A10;
hence  q [= b by A8, A10, A11; ::_thesis: verum
end;
 (f,O1) +. a = "\/" ((rng L1),L) by A6, A8, Th17;
hence  S1[O1] by A9, LATTICE3:def_21; ::_thesis: verum
end;
A12: S1[ {} ] by A1, Th13;
thus  for O2 being Ordinal holds S1[O2] from ORDINAL2:sch_1(A12, A4, A5); ::_thesis: verum
end;

theorem Th35: :: KNASTER:35
for L being complete Lattice
for f being monotone UnOp of L
for b, a being Element of L st b [= a & b is_a_fixpoint_of f holds
for O2 being Ordinal holds b [= (f,O2) -. a
proof
let L be complete Lattice; ::_thesis: for f being monotone UnOp of L
for b, a being Element of L st b [= a & b is_a_fixpoint_of f holds
for O2 being Ordinal holds b [= (f,O2) -. a
let f be monotone UnOp of L; ::_thesis: for b, a being Element of L st b [= a & b is_a_fixpoint_of f holds
for O2 being Ordinal holds b [= (f,O2) -. a
let b, a be Element of L; ::_thesis: ( b [= a & b is_a_fixpoint_of f implies for O2 being Ordinal holds b [= (f,O2) -. a )
assume that
A1: b [= a and
A2: b is_a_fixpoint_of f ; ::_thesis: for O2 being Ordinal holds b [= (f,O2) -. a
defpred S1[ Ordinal] means b [= (f,$1) -. a;
A3: f . b = b by A2, ABIAN:def_3;
A4: now__::_thesis:_for_O1_being_Ordinal_st_S1[O1]_holds_
S1[_succ_O1]
let O1 be Ordinal; ::_thesis: ( S1[O1] implies S1[ succ O1] )
assume  S1[O1] ; ::_thesis: S1[ succ O1]
then  f . b [= f . ((f,O1) -. a) by QUANTAL1:def_12;
hence  S1[ succ O1] by A3, Th16; ::_thesis: verum
end;
A5: now__::_thesis:_for_O1_being_Ordinal_st_O1_<>_{}_&_O1_is_limit_ordinal_&_(_for_O2_being_Ordinal_st_O2_in_O1_holds_
S1[O2]_)_holds_
S1[O1]
deffunc H1( Ordinal) ->  Element of L = (f,$1) -. a;
let O1 be Ordinal; ::_thesis: ( O1 <> {} & O1 is limit_ordinal & ( for O2 being Ordinal st O2 in O1 holds
S1[O2] ) implies S1[O1] )
assume that
A6: ( O1 <> {} & O1 is limit_ordinal ) and
A7: for O2 being Ordinal st O2 in O1 holds
S1[O2] ; ::_thesis: S1[O1]
consider L1 being T-Sequence such that
A8: ( dom L1 = O1 & ( for O3 being Ordinal st O3 in O1 holds
L1 . O3 = H1(O3) ) ) from ORDINAL2:sch_2();
A9: b is_less_than rng L1
proof
let q be Element of L; :: according to LATTICE3:def_16 ::_thesis: ( not q in rng L1 or b [= q )
assume  q in rng L1 ; ::_thesis: b [= q
then consider O3 being set  such that
A10: O3 in dom L1 and
A11: q = L1 . O3 by FUNCT_1:def_3;
reconsider O3 = O3 as Ordinal by A10;
 b [= (f,O3) -. a by A7, A8, A10;
hence  b [= q by A8, A10, A11; ::_thesis: verum
end;
 (f,O1) -. a = "/\" ((rng L1),L) by A6, A8, Th18;
hence  S1[O1] by A9, LATTICE3:39; ::_thesis: verum
end;
A12: S1[ {} ] by A1, Th14;
thus  for O2 being Ordinal holds S1[O2] from ORDINAL2:sch_1(A12, A4, A5); ::_thesis: verum
end;

definition
let L be complete Lattice;
let f be UnOp of L;
assume B1: f is monotone ;
func FixPoints f ->  strict Lattice means :Def9: :: KNASTER:def 9
 ex P being non empty with_suprema with_infima Subset of L st
( P =  {  x where x is Element of L : x is_a_fixpoint_of f  }  & it = latt P );
existence
 ex b1 being strict Lattice ex P being non empty with_suprema with_infima Subset of L st
( P =  {  x where x is Element of L : x is_a_fixpoint_of f  }  & b1 = latt P )
proof
defpred S1[ set ] means $1 is_a_fixpoint_of f;
set P =  {  x where x is Element of L : S1[x]  }  ;
A1:  {  x where x is Element of L : S1[x]  }  is Subset of L from DOMAIN_1:sch_7();
consider a being Element of L such that
A2: a is_a_fixpoint_of f by B1, Th21;
A3: a in  {  x where x is Element of L : S1[x]  }  by A2;
reconsider P =  {  x where x is Element of L : S1[x]  }  as Subset of L by A1;
A4: P is with_suprema
proof
let x, y be Element of L; :: according to KNASTER:def_6 ::_thesis: ( x in P & y in P implies ex z being Element of L st
( z in P & x [= z & y [= z & ( for z9 being Element of L st z9 in P & x [= z9 & y [= z9 holds
z [= z9 ) ) )
assume that
A5: x in P and
A6: y in P ; ::_thesis: ex z being Element of L st
( z in P & x [= z & y [= z & ( for z9 being Element of L st z9 in P & x [= z9 & y [= z9 holds
z [= z9 ) )
consider a being Element of L such that
A7: x = a and
A8: a is_a_fixpoint_of f by A5;
consider b being Element of L such that
A9: y = b and
A10: b is_a_fixpoint_of f by A6;
reconsider a = a, b = b as Element of L ;
reconsider ab = a "\/" b as Element of L ;
consider O being Ordinal such that
 card O c= card the carrier of L and
A11: (f,O) +. ab is_a_fixpoint_of f and
A12: ( a [= (f,O) +. ab & b [= (f,O) +. ab ) by B1, A8, A10, Th32;
set z = (f,O) +. ab;
take  (f,O) +. ab ; ::_thesis: ( (f,O) +. ab in P & x [= (f,O) +. ab & y [= (f,O) +. ab & ( for z9 being Element of L st z9 in P & x [= z9 & y [= z9 holds
(f,O) +. ab [= z9 ) )
thus  (f,O) +. ab in P by A11; ::_thesis: ( x [= (f,O) +. ab & y [= (f,O) +. ab & ( for z9 being Element of L st z9 in P & x [= z9 & y [= z9 holds
(f,O) +. ab [= z9 ) )
thus  ( x [= (f,O) +. ab & y [= (f,O) +. ab ) by A7, A9, A12; ::_thesis: for z9 being Element of L st z9 in P & x [= z9 & y [= z9 holds
(f,O) +. ab [= z9
let z9 be Element of L; ::_thesis: ( z9 in P & x [= z9 & y [= z9 implies (f,O) +. ab [= z9 )
assume that
A13: z9 in P and
A14: ( x [= z9 & y [= z9 ) ; ::_thesis: (f,O) +. ab [= z9
A15: ex zz being Element of L st
( zz = z9 & zz is_a_fixpoint_of f ) by A13;
 ab [= z9 by A7, A9, A14, FILTER_0:6;
hence  (f,O) +. ab [= z9 by B1, A15, Th34; ::_thesis: verum
end;
 P is with_infima
proof
let x, y be Element of L; :: according to KNASTER:def_7 ::_thesis: ( x in P & y in P implies ex z being Element of L st
( z in P & z [= x & z [= y & ( for z9 being Element of L st z9 in P & z9 [= x & z9 [= y holds
z9 [= z ) ) )
assume that
A16: x in P and
A17: y in P ; ::_thesis: ex z being Element of L st
( z in P & z [= x & z [= y & ( for z9 being Element of L st z9 in P & z9 [= x & z9 [= y holds
z9 [= z ) )
consider a being Element of L such that
A18: x = a and
A19: a is_a_fixpoint_of f by A16;
consider b being Element of L such that
A20: y = b and
A21: b is_a_fixpoint_of f by A17;
reconsider a = a, b = b as Element of L ;
reconsider ab = a "/\" b as Element of L ;
consider O being Ordinal such that
 card O c= card the carrier of L and
A22: (f,O) -. ab is_a_fixpoint_of f and
A23: ( (f,O) -. ab [= a & (f,O) -. ab [= b ) by B1, A19, A21, Th33;
set z = (f,O) -. ab;
take  (f,O) -. ab ; ::_thesis: ( (f,O) -. ab in P & (f,O) -. ab [= x & (f,O) -. ab [= y & ( for z9 being Element of L st z9 in P & z9 [= x & z9 [= y holds
z9 [= (f,O) -. ab ) )
thus  (f,O) -. ab in P by A22; ::_thesis: ( (f,O) -. ab [= x & (f,O) -. ab [= y & ( for z9 being Element of L st z9 in P & z9 [= x & z9 [= y holds
z9 [= (f,O) -. ab ) )
thus  ( (f,O) -. ab [= x & (f,O) -. ab [= y ) by A18, A20, A23; ::_thesis: for z9 being Element of L st z9 in P & z9 [= x & z9 [= y holds
z9 [= (f,O) -. ab
let z9 be Element of L; ::_thesis: ( z9 in P & z9 [= x & z9 [= y implies z9 [= (f,O) -. ab )
assume that
A24: z9 in P and
A25: ( z9 [= x & z9 [= y ) ; ::_thesis: z9 [= (f,O) -. ab
A26: ex zz being Element of L st
( zz = z9 & zz is_a_fixpoint_of f ) by A24;
 z9 [= ab by A18, A20, A25, FILTER_0:7;
hence  z9 [= (f,O) -. ab by B1, A26, Th35; ::_thesis: verum
end;
then reconsider P = P as non empty with_suprema with_infima Subset of L by A3, A4;
take  latt P ; ::_thesis: ex P being non empty with_suprema with_infima Subset of L st
( P =  {  x where x is Element of L : x is_a_fixpoint_of f  }  & latt P = latt P )
take  P ; ::_thesis: ( P =  {  x where x is Element of L : x is_a_fixpoint_of f  }  & latt P = latt P )
thus  P =  {  x where x is Element of L : x is_a_fixpoint_of f  }  ; ::_thesis: latt P = latt P
thus  latt P = latt P ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict Lattice st ex P being non empty with_suprema with_infima Subset of L st
( P =  {  x where x is Element of L : x is_a_fixpoint_of f  }  & b1 = latt P ) & ex P being non empty with_suprema with_infima Subset of L st
( P =  {  x where x is Element of L : x is_a_fixpoint_of f  }  & b2 = latt P ) holds
b1 = b2 ;
end;

:: deftheorem Def9 defines FixPoints KNASTER:def_9_:_
 for L being complete Lattice
for f being UnOp of L st f is monotone holds
for b3 being strict Lattice holds
( b3 = FixPoints f iff ex P being non empty with_suprema with_infima Subset of L st
( P =  {  x where x is Element of L : x is_a_fixpoint_of f  }  & b3 = latt P ) );

theorem Th36: :: KNASTER:36
for L being complete Lattice
for f being monotone UnOp of L holds the carrier of (FixPoints f) =  {  x where x is Element of L : x is_a_fixpoint_of f  }
proof
let L be complete Lattice; ::_thesis: for f being monotone UnOp of L holds the carrier of (FixPoints f) =  {  x where x is Element of L : x is_a_fixpoint_of f  }
let f be monotone UnOp of L; ::_thesis: the carrier of (FixPoints f) =  {  x where x is Element of L : x is_a_fixpoint_of f  }
 ex P being non empty with_suprema with_infima Subset of L st
( P =  {  x where x is Element of L : x is_a_fixpoint_of f  }  & FixPoints f = latt P ) by Def9;
hence  the carrier of (FixPoints f) =  {  x where x is Element of L : x is_a_fixpoint_of f  }  by Def8; ::_thesis: verum
end;

theorem Th37: :: KNASTER:37
for L being complete Lattice
for f being monotone UnOp of L holds the carrier of (FixPoints f) c= the carrier of L
proof
let L be complete Lattice; ::_thesis: for f being monotone UnOp of L holds the carrier of (FixPoints f) c= the carrier of L
let f be monotone UnOp of L; ::_thesis: the carrier of (FixPoints f) c= the carrier of L
A1: the carrier of (FixPoints f) =  {  x where x is Element of L : x is_a_fixpoint_of f  }  by Th36;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (FixPoints f) or x in the carrier of L )
assume  x in the carrier of (FixPoints f) ; ::_thesis: x in the carrier of L
then  ex a being Element of L st
( x = a & a is_a_fixpoint_of f ) by A1;
hence  x in the carrier of L ; ::_thesis: verum
end;

theorem Th38: :: KNASTER:38
for L being complete Lattice
for f being monotone UnOp of L
for a being Element of L holds
( a in the carrier of (FixPoints f) iff a is_a_fixpoint_of f )
proof
let L be complete Lattice; ::_thesis: for f being monotone UnOp of L
for a being Element of L holds
( a in the carrier of (FixPoints f) iff a is_a_fixpoint_of f )
let f be monotone UnOp of L; ::_thesis: for a being Element of L holds
( a in the carrier of (FixPoints f) iff a is_a_fixpoint_of f )
let a be Element of L; ::_thesis: ( a in the carrier of (FixPoints f) iff a is_a_fixpoint_of f )
A1: the carrier of (FixPoints f) =  {  x where x is Element of L : x is_a_fixpoint_of f  }  by Th36;
hereby  ::_thesis: ( a is_a_fixpoint_of f implies a in the carrier of (FixPoints f) )
assume  a in the carrier of (FixPoints f) ; ::_thesis: a is_a_fixpoint_of f
then  ex b being Element of L st
( a = b & b is_a_fixpoint_of f ) by A1;
hence  a is_a_fixpoint_of f ; ::_thesis: verum
end;
assume  a is_a_fixpoint_of f ; ::_thesis: a in the carrier of (FixPoints f)
hence  a in the carrier of (FixPoints f) by A1; ::_thesis: verum
end;

theorem Th39: :: KNASTER:39
for L being complete Lattice
for f being monotone UnOp of L
for x, y being Element of (FixPoints f)
for a, b being Element of L st x = a & y = b holds
( x [= y iff a [= b )
proof
let L be complete Lattice; ::_thesis: for f being monotone UnOp of L
for x, y being Element of (FixPoints f)
for a, b being Element of L st x = a & y = b holds
( x [= y iff a [= b )
let f be monotone UnOp of L; ::_thesis: for x, y being Element of (FixPoints f)
for a, b being Element of L st x = a & y = b holds
( x [= y iff a [= b )
A1: ex P being non empty with_suprema with_infima Subset of L st
( P =  {  x where x is Element of L : x is_a_fixpoint_of f  }  & FixPoints f = latt P ) by Def9;
let x, y be Element of (FixPoints f); ::_thesis: for a, b being Element of L st x = a & y = b holds
( x [= y iff a [= b )
let a, b be Element of L; ::_thesis: ( x = a & y = b implies ( x [= y iff a [= b ) )
assume A2: ( x = a & y = b ) ; ::_thesis: ( x [= y iff a [= b )
 ex a9, b9 being Element of L st
( x = a9 & y = b9 & ( x [= y implies a9 [= b9 ) & ( a9 [= b9 implies x [= y ) ) by A1, Def8;
hence  ( x [= y iff a [= b ) by A2; ::_thesis: verum
end;

theorem :: KNASTER:40
for L being complete Lattice
for f being monotone UnOp of L holds FixPoints f is complete
proof
let L be complete Lattice; ::_thesis: for f being monotone UnOp of L holds FixPoints f is complete
let f be monotone UnOp of L; ::_thesis: FixPoints f is complete
set F = FixPoints f;
set cF = the carrier of (FixPoints f);
set cL = the carrier of L;
let X be set ; :: according to LATTICE3:def_18 ::_thesis: ex b1 being Element of the carrier of (FixPoints f) st
( X is_less_than b1 & ( for b2 being Element of the carrier of (FixPoints f) holds
( not X is_less_than b2 or b1 [= b2 ) ) )
set Y = X /\ the carrier of (FixPoints f);
set s = "\/" ((X /\ the carrier of (FixPoints f)),L);
A1: X /\ the carrier of (FixPoints f) c= the carrier of (FixPoints f) by XBOOLE_1:17;
 X /\ the carrier of (FixPoints f) is_less_than f . ("\/" ((X /\ the carrier of (FixPoints f)),L))
proof
let q be Element of the carrier of L; :: according to LATTICE3:def_17 ::_thesis: ( not q in X /\ the carrier of (FixPoints f) or q [= f . ("\/" ((X /\ the carrier of (FixPoints f)),L)) )
reconsider q9 = q as Element of L ;
assume A2: q in X /\ the carrier of (FixPoints f) ; ::_thesis: q [= f . ("\/" ((X /\ the carrier of (FixPoints f)),L))
then  q [= "\/" ((X /\ the carrier of (FixPoints f)),L) by LATTICE3:38;
then A3: f . q [= f . ("\/" ((X /\ the carrier of (FixPoints f)),L)) by QUANTAL1:def_12;
 q9 is_a_fixpoint_of f by A1, A2, Th38;
hence  q [= f . ("\/" ((X /\ the carrier of (FixPoints f)),L)) by A3, ABIAN:def_3; ::_thesis: verum
end;
then A4: "\/" ((X /\ the carrier of (FixPoints f)),L) [= f . ("\/" ((X /\ the carrier of (FixPoints f)),L)) by LATTICE3:def_21;
then consider O being Ordinal such that
 card O c= card the carrier of L and
A5: (f,O) +. ("\/" ((X /\ the carrier of (FixPoints f)),L)) is_a_fixpoint_of f by Th30;
reconsider p9 = (f,O) +. ("\/" ((X /\ the carrier of (FixPoints f)),L)) as Element of L ;
reconsider p = p9 as Element of the carrier of (FixPoints f) by A5, Th38;
take  p ; ::_thesis: ( X is_less_than p & ( for b1 being Element of the carrier of (FixPoints f) holds
( not X is_less_than b1 or p [= b1 ) ) )
thus  X is_less_than p ::_thesis: for b1 being Element of the carrier of (FixPoints f) holds
( not X is_less_than b1 or p [= b1 )
proof
let q be Element of the carrier of (FixPoints f); :: according to LATTICE3:def_17 ::_thesis: ( not q in X or q [= p )
 ( q in the carrier of (FixPoints f) & the carrier of (FixPoints f) c= the carrier of L ) by Th37;
then reconsider qL9 = q as Element of L ;
assume  q in X ; ::_thesis: q [= p
then  q in X /\ the carrier of (FixPoints f) by XBOOLE_0:def_4;
then A6: qL9 [= "\/" ((X /\ the carrier of (FixPoints f)),L) by LATTICE3:38;
 "\/" ((X /\ the carrier of (FixPoints f)),L) [= p9 by A4, Th22;
then  qL9 [= p9 by A6, LATTICES:7;
hence  q [= p by Th39; ::_thesis: verum
end;
let r be Element of the carrier of (FixPoints f); ::_thesis: ( not X is_less_than r or p [= r )
assume A7: X is_less_than r ; ::_thesis: p [= r
reconsider r99 = r as Element of (FixPoints f) ;
 ( the carrier of (FixPoints f) =  {  x where x is Element of L : x is_a_fixpoint_of f  }  & r in the carrier of (FixPoints f) ) by Th36;
then consider r9 being Element of L such that
A8: r9 = r and
A9: r9 is_a_fixpoint_of f ;
A10: X /\ the carrier of (FixPoints f) c= X by XBOOLE_1:17;
 X /\ the carrier of (FixPoints f) is_less_than r9
proof
let q be Element of the carrier of L; :: according to LATTICE3:def_17 ::_thesis: ( not q in X /\ the carrier of (FixPoints f) or q [= r9 )
assume A11: q in X /\ the carrier of (FixPoints f) ; ::_thesis: q [= r9
then reconsider q99 = q as Element of (FixPoints f) by A1;
 q99 [= r99 by A10, A7, A11, LATTICE3:def_17;
hence  q [= r9 by A8, Th39; ::_thesis: verum
end;
then  "\/" ((X /\ the carrier of (FixPoints f)),L) [= r9 by LATTICE3:def_21;
then  p9 [= r9 by A9, Th34;
hence  p [= r by A8, Th39; ::_thesis: verum
end;

definition
let L be complete Lattice;
let f be monotone UnOp of L;
func lfp f ->  Element of L equals :: KNASTER:def 10
(f,(nextcard the carrier of L)) +. (Bottom L);
coherence
 (f,(nextcard the carrier of L)) +. (Bottom L) is Element of L ;
func gfp f ->  Element of L equals :: KNASTER:def 11
(f,(nextcard the carrier of L)) -. (Top L);
coherence
 (f,(nextcard the carrier of L)) -. (Top L) is Element of L ;
end;

:: deftheorem  defines lfp KNASTER:def_10_:_
 for L being complete Lattice
for f being monotone UnOp of L holds lfp f = (f,(nextcard the carrier of L)) +. (Bottom L);

:: deftheorem  defines gfp KNASTER:def_11_:_
 for L being complete Lattice
for f being monotone UnOp of L holds gfp f = (f,(nextcard the carrier of L)) -. (Top L);

theorem Th41: :: KNASTER:41
for L being complete Lattice
for f being monotone UnOp of L holds
( lfp f is_a_fixpoint_of f & ex O being Ordinal st
( card O c= card the carrier of L & (f,O) +. (Bottom L) = lfp f ) )
proof
let L be complete Lattice; ::_thesis: for f being monotone UnOp of L holds
( lfp f is_a_fixpoint_of f & ex O being Ordinal st
( card O c= card the carrier of L & (f,O) +. (Bottom L) = lfp f ) )
let f be monotone UnOp of L; ::_thesis: ( lfp f is_a_fixpoint_of f & ex O being Ordinal st
( card O c= card the carrier of L & (f,O) +. (Bottom L) = lfp f ) )
reconsider ze = Bottom L as Element of L ;
A1: Bottom L [= f . ze by LATTICES:16;
then consider O being Ordinal 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; ::_thesis: ex O being Ordinal st
( card O c= card the carrier of L & (f,O) +. (Bottom L) = lfp f )
take  O ; ::_thesis: ( card O c= card the carrier of L & (f,O) +. (Bottom L) = lfp f )
thus  card O c= card the carrier of L by A2; ::_thesis: (f,O) +. (Bottom L) = lfp f
thus  (f,O) +. (Bottom L) = lfp f by A1, A3, A4, Th28; ::_thesis: verum
end;

theorem Th42: :: KNASTER:42
for L being complete Lattice
for f being monotone UnOp of L holds
( gfp f is_a_fixpoint_of f & ex O being Ordinal st
( card O c= card the carrier of L & (f,O) -. (Top L) = gfp f ) )
proof
let L be complete Lattice; ::_thesis: for f being monotone UnOp of L holds
( gfp f is_a_fixpoint_of f & ex O being Ordinal st
( card O c= card the carrier of L & (f,O) -. (Top L) = gfp f ) )
let f be monotone UnOp of L; ::_thesis: ( gfp f is_a_fixpoint_of f & ex O being Ordinal st
( card O c= card the carrier of L & (f,O) -. (Top L) = gfp f ) )
reconsider je = Top L as Element of L ;
A1: f . je [= Top L by LATTICES:19;
then consider O being Ordinal 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; ::_thesis: ex O being Ordinal st
( card O c= card the carrier of L & (f,O) -. (Top L) = gfp f )
take  O ; ::_thesis: ( card O c= card the carrier of L & (f,O) -. (Top L) = gfp f )
thus  card O c= card the carrier of L by A2; ::_thesis: (f,O) -. (Top L) = gfp f
thus  (f,O) -. (Top L) = gfp f by A1, A3, A4, Th29; ::_thesis: verum
end;

theorem Th43: :: KNASTER:43
for L being complete Lattice
for f being monotone UnOp of L
for a being Element of L st a is_a_fixpoint_of f holds
( lfp f [= a & a [= gfp f )
proof
let L be complete Lattice; ::_thesis: for f being monotone UnOp of L
for a being Element of L st a is_a_fixpoint_of f holds
( lfp f [= a & a [= gfp f )
let f be monotone UnOp of L; ::_thesis: for a being Element of L st a is_a_fixpoint_of f holds
( lfp f [= a & a [= gfp f )
let a be Element of L; ::_thesis: ( a is_a_fixpoint_of f implies ( lfp f [= a & a [= gfp f ) )
defpred S1[ Ordinal] means (f,$1) +. (Bottom L) [= a;
A1: now__::_thesis:_for_O1_being_Ordinal_st_O1_<>_{}_&_O1_is_limit_ordinal_&_(_for_O2_being_Ordinal_st_O2_in_O1_holds_
S1[O2]_)_holds_
S1[O1]
deffunc H1( Ordinal) ->  Element of L = (f,$1) +. (Bottom L);
let O1 be Ordinal; ::_thesis: ( O1 <> {} & O1 is limit_ordinal & ( for O2 being Ordinal st O2 in O1 holds
S1[O2] ) implies S1[O1] )
assume that
A2: ( O1 <> {} & O1 is limit_ordinal ) and
A3: for O2 being Ordinal st O2 in O1 holds
S1[O2] ; ::_thesis: S1[O1]
consider L1 being T-Sequence such that
A4: ( dom L1 = O1 & ( for O3 being Ordinal st O3 in O1 holds
L1 . O3 = H1(O3) ) ) from ORDINAL2:sch_2();
A5: rng L1 is_less_than a
proof
let q be Element of L; :: according to LATTICE3:def_17 ::_thesis: ( not q in rng L1 or q [= a )
assume  q in rng L1 ; ::_thesis: q [= a
then consider C being set  such that
A6: C in dom L1 and
A7: q = L1 . C by FUNCT_1:def_3;
reconsider C = C as Ordinal by A6;
 (f,C) +. (Bottom L) [= a by A3, A4, A6;
hence  q [= a by A4, A6, A7; ::_thesis: verum
end;
 (f,O1) +. (Bottom L) = "\/" ((rng L1),L) by A2, A4, Th17;
hence  S1[O1] by A5, LATTICE3:def_21; ::_thesis: verum
end;
assume  a is_a_fixpoint_of f ; ::_thesis: ( lfp f [= a & a [= gfp f )
then A8: f . a = a by ABIAN:def_3;
A9: now__::_thesis:_for_O1_being_Ordinal_st_S1[O1]_holds_
S1[_succ_O1]
let O1 be Ordinal; ::_thesis: ( S1[O1] implies S1[ succ O1] )
assume  S1[O1] ; ::_thesis: S1[ succ O1]
then  f . ((f,O1) +. (Bottom L)) [= f . a by QUANTAL1:def_12;
hence  S1[ succ O1] by A8, Th15; ::_thesis: verum
end;
 (f,{}) +. (Bottom L) = Bottom L by Th13;
then A10: S1[ {} ] by LATTICES:16;
 for O2 being Ordinal holds S1[O2] from ORDINAL2:sch_1(A10, A9, A1);
hence  lfp f [= a ; ::_thesis: a [= gfp f
defpred S2[ Ordinal] means a [= (f,$1) -. (Top L);
A11: now__::_thesis:_for_O1_being_Ordinal_st_S2[O1]_holds_
S2[_succ_O1]
let O1 be Ordinal; ::_thesis: ( S2[O1] implies S2[ succ O1] )
assume  S2[O1] ; ::_thesis: S2[ succ O1]
then  f . a [= f . ((f,O1) -. (Top L)) by QUANTAL1:def_12;
hence  S2[ succ O1] by A8, Th16; ::_thesis: verum
end;
A12: now__::_thesis:_for_O1_being_Ordinal_st_O1_<>_{}_&_O1_is_limit_ordinal_&_(_for_O2_being_Ordinal_st_O2_in_O1_holds_
S2[O2]_)_holds_
S2[O1]
deffunc H1( Ordinal) ->  Element of L = (f,$1) -. (Top L);
let O1 be Ordinal; ::_thesis: ( O1 <> {} & O1 is limit_ordinal & ( for O2 being Ordinal st O2 in O1 holds
S2[O2] ) implies S2[O1] )
assume that
A13: ( O1 <> {} & O1 is limit_ordinal ) and
A14: for O2 being Ordinal st O2 in O1 holds
S2[O2] ; ::_thesis: S2[O1]
consider L1 being T-Sequence such that
A15: ( dom L1 = O1 & ( for O3 being Ordinal st O3 in O1 holds
L1 . O3 = H1(O3) ) ) from ORDINAL2:sch_2();
A16: a is_less_than rng L1
proof
let q be Element of L; :: according to LATTICE3:def_16 ::_thesis: ( not q in rng L1 or a [= q )
assume  q in rng L1 ; ::_thesis: a [= q
then consider C being set  such that
A17: C in dom L1 and
A18: q = L1 . C by FUNCT_1:def_3;
reconsider C = C as Ordinal by A17;
 a [= (f,C) -. (Top L) by A14, A15, A17;
hence  a [= q by A15, A17, A18; ::_thesis: verum
end;
 (f,O1) -. (Top L) = "/\" ((rng L1),L) by A13, A15, Th18;
hence  S2[O1] by A16, LATTICE3:39; ::_thesis: verum
end;
 (f,{}) -. (Top L) = Top L by Th14;
then A19: S2[ {} ] by LATTICES:19;
 for O2 being Ordinal holds S2[O2] from ORDINAL2:sch_1(A19, A11, A12);
hence  a [= gfp f ; ::_thesis: verum
end;

theorem :: KNASTER:44
for L being complete Lattice
for f being monotone UnOp of L
for a being Element of L st f . a [= a holds
lfp f [= a
proof
let L be complete Lattice; ::_thesis: for f being monotone UnOp of L
for a being Element of L st f . a [= a holds
lfp f [= a
let f be monotone UnOp of L; ::_thesis: for a being Element of L st f . a [= a holds
lfp f [= a
let a be Element of L; ::_thesis: ( f . a [= a implies lfp f [= a )
assume A1: f . a [= a ; ::_thesis: lfp f [= a
then consider O being Ordinal 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  lfp f [= a by A3, LATTICES:7; ::_thesis: verum
end;

theorem :: KNASTER:45
for L being complete Lattice
for f being monotone UnOp of L
for a being Element of L st a [= f . a holds
a [= gfp f
proof
let L be complete Lattice; ::_thesis: for f being monotone UnOp of L
for a being Element of L st a [= f . a holds
a [= gfp f
let f be monotone UnOp of L; ::_thesis: for a being Element of L st a [= f . a holds
a [= gfp f
let a be Element of L; ::_thesis: ( a [= f . a implies a [= gfp f )
assume A1: a [= f . a ; ::_thesis: a [= gfp f
then consider O being Ordinal 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  a [= gfp f by A3, LATTICES:7; ::_thesis: verum
end;

begin

theorem Th46: :: KNASTER:46
for A being non empty set
for f being UnOp of (BooleLatt A) holds
( f is monotone iff f is V220() )
proof
let A be non empty set ; ::_thesis: for f being UnOp of (BooleLatt A) holds
( f is monotone iff f is V220() )
let f be UnOp of (BooleLatt A); ::_thesis: ( f is monotone iff f is V220() )
thus  ( f is monotone implies f is V220() ) ::_thesis: ( f is V220() implies f is monotone )
proof
assume A1: f is monotone ; ::_thesis: f is V220()
let x, y be Element of (BooleLatt A); :: according to KNASTER:def_1 ::_thesis: ( x c= y implies f . x c= f . y )
assume  x c= y ; ::_thesis: f . x c= f . y
then  x [= y by LATTICE3:2;
then  f . x [= f . y by A1, QUANTAL1:def_12;
hence  f . x c= f . y by LATTICE3:2; ::_thesis: verum
end;
assume A2: f is V220() ; ::_thesis: f is monotone
let p, q be Element of (BooleLatt A); :: according to QUANTAL1:def_12 ::_thesis: ( not p [= q or f . p [= f . q )
assume  p [= q ; ::_thesis: f . p [= f . q
then  p c= q by LATTICE3:2;
then  f . p c= f . q by A2, Def1;
hence  f . p [= f . q by LATTICE3:2; ::_thesis: verum
end;

theorem :: KNASTER:47
for A being non empty set
for f being monotone UnOp of (BooleLatt A) ex g being V220() Function of (bool A),(bool A) st lfp (A,g) = lfp f
proof
let A be non empty set ; ::_thesis: for f being monotone UnOp of (BooleLatt A) ex g being V220() Function of (bool A),(bool A) st lfp (A,g) = lfp f
let f be monotone UnOp of (BooleLatt A); ::_thesis: ex g being V220() Function of (bool A),(bool A) st lfp (A,g) = lfp f
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 V220() Function of (bool A),(bool A) by Th46;
reconsider lg = lfp (A,g) as Element of (BooleLatt A) by LATTICE3:def_1;
take  g ; ::_thesis: lfp (A,g) = lfp f
 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  lfp (A,g) = lfp f by A1, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: KNASTER:48
for A being non empty set
for f being monotone UnOp of (BooleLatt A) ex g being V220() Function of (bool A),(bool A) st gfp (A,g) = gfp f
proof
let A be non empty set ; ::_thesis: for f being monotone UnOp of (BooleLatt A) ex g being V220() Function of (bool A),(bool A) st gfp (A,g) = gfp f
let f be monotone UnOp of (BooleLatt A); ::_thesis: ex g being V220() Function of (bool A),(bool A) st gfp (A,g) = gfp f
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 V220() Function of (bool A),(bool A) by Th46;
reconsider gg = gfp (A,g) as Element of (BooleLatt A) by LATTICE3:def_1;
take  g ; ::_thesis: gfp (A,g) = gfp f
 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  gfp (A,g) = gfp f by A1, XBOOLE_0:def_10; ::_thesis: verum
end;