:: WAYBEL22 semantic presentation

begin

Lm1:  for L being complete LATTICE
for X being set st X c= bool the carrier of L holds
"/\" ((union X),L) = "/\" ( {  (inf Y) where Y is Subset of L : Y in X  }  ,L)
proof
let L be complete LATTICE; ::_thesis: for X being set st X c= bool the carrier of L holds
"/\" ((union X),L) = "/\" ( {  (inf Y) where Y is Subset of L : Y in X  }  ,L)
let X be set ; ::_thesis: ( X c= bool the carrier of L implies "/\" ((union X),L) = "/\" ( {  (inf Y) where Y is Subset of L : Y in X  }  ,L) )
assume A1: X c= bool the carrier of L ; ::_thesis: "/\" ((union X),L) = "/\" ( {  (inf Y) where Y is Subset of L : Y in X  }  ,L)
defpred S1[ Subset of L] means $1 in X;
set XX =  {  Z where Z is Subset of L : S1[Z]  }  ;
A2: now__::_thesis:_for_x_being_set_holds_
(_(_x_in__{__Z_where_Z_is_Subset_of_L_:_S1[Z]__}__implies_x_in_X_)_&_(_x_in_X_implies_x_in__{__Z_where_Z_is_Subset_of_L_:_S1[Z]__}__)_)
let x be set ; ::_thesis: ( ( x in  {  Z where Z is Subset of L : S1[Z]  }  implies x in X ) & ( x in X implies x in  {  Z where Z is Subset of L : S1[Z]  }  ) )
hereby  ::_thesis: ( x in X implies x in  {  Z where Z is Subset of L : S1[Z]  }  )
assume  x in  {  Z where Z is Subset of L : S1[Z]  }  ; ::_thesis: x in X
then  ex Z being Subset of L st
( x = Z & Z in X ) ;
hence  x in X ; ::_thesis: verum
end;
assume A3: x in X ; ::_thesis: x in  {  Z where Z is Subset of L : S1[Z]  }
then reconsider x9 = x as Subset of L by A1;
 x9 in  {  Z where Z is Subset of L : S1[Z]  }  by A3;
hence  x in  {  Z where Z is Subset of L : S1[Z]  }  ; ::_thesis: verum
end;
 "/\" ( {  ("/\" (Y,L)) where Y is Subset of L : S1[Y]  }  ,L) = "/\" ((union  {  Z where Z is Subset of L : S1[Z]  }  ),L) from YELLOW_3:sch_3();
hence  "/\" ((union X),L) = "/\" ( {  (inf Y) where Y is Subset of L : Y in X  }  ,L) by A2, TARSKI:1; ::_thesis: verum
end;

Lm2:  for L being complete LATTICE
for X being set st X c= bool the carrier of L holds
"\/" ((union X),L) = "\/" ( {  (sup Y) where Y is Subset of L : Y in X  }  ,L)
proof
let L be complete LATTICE; ::_thesis: for X being set st X c= bool the carrier of L holds
"\/" ((union X),L) = "\/" ( {  (sup Y) where Y is Subset of L : Y in X  }  ,L)
let X be set ; ::_thesis: ( X c= bool the carrier of L implies "\/" ((union X),L) = "\/" ( {  (sup Y) where Y is Subset of L : Y in X  }  ,L) )
assume A1: X c= bool the carrier of L ; ::_thesis: "\/" ((union X),L) = "\/" ( {  (sup Y) where Y is Subset of L : Y in X  }  ,L)
defpred S1[ set ] means $1 in X;
set XX =  {  Z where Z is Subset of L : S1[Z]  }  ;
A2: now__::_thesis:_for_x_being_set_holds_
(_(_x_in__{__Z_where_Z_is_Subset_of_L_:_S1[Z]__}__implies_x_in_X_)_&_(_x_in_X_implies_x_in__{__Z_where_Z_is_Subset_of_L_:_S1[Z]__}__)_)
let x be set ; ::_thesis: ( ( x in  {  Z where Z is Subset of L : S1[Z]  }  implies x in X ) & ( x in X implies x in  {  Z where Z is Subset of L : S1[Z]  }  ) )
hereby  ::_thesis: ( x in X implies x in  {  Z where Z is Subset of L : S1[Z]  }  )
assume  x in  {  Z where Z is Subset of L : S1[Z]  }  ; ::_thesis: x in X
then  ex Z being Subset of L st
( x = Z & Z in X ) ;
hence  x in X ; ::_thesis: verum
end;
assume A3: x in X ; ::_thesis: x in  {  Z where Z is Subset of L : S1[Z]  }
then reconsider x9 = x as Subset of L by A1;
 x9 in  {  Z where Z is Subset of L : S1[Z]  }  by A3;
hence  x in  {  Z where Z is Subset of L : S1[Z]  }  ; ::_thesis: verum
end;
 "\/" ( {  ("\/" (Y,L)) where Y is Subset of L : S1[Y]  }  ,L) = "\/" ((union  {  Z where Z is Subset of L : S1[Z]  }  ),L) from YELLOW_3:sch_5();
hence  "\/" ((union X),L) = "\/" ( {  (sup Y) where Y is Subset of L : Y in X  }  ,L) by A2, TARSKI:1; ::_thesis: verum
end;

theorem Th1: :: WAYBEL22:1
for L being upper-bounded Semilattice
for F being non empty directed Subset of (InclPoset (Filt L)) holds sup F = union F
proof
let L be upper-bounded Semilattice; ::_thesis: for F being non empty directed Subset of (InclPoset (Filt L)) holds sup F = union F
let F be non empty directed Subset of (InclPoset (Filt L)); ::_thesis: sup F = union F
 Filt L = Ids (L opp) by WAYBEL16:7;
hence  sup F = union F by WAYBEL13:9; ::_thesis: verum
end;

theorem Th2: :: WAYBEL22:2
for L, S, T being non empty complete Poset
for f being CLHomomorphism of L,S
for g being CLHomomorphism of S,T holds g * f is CLHomomorphism of L,T
proof
let L, S, T be non empty complete Poset; ::_thesis: for f being CLHomomorphism of L,S
for g being CLHomomorphism of S,T holds g * f is CLHomomorphism of L,T
let f be CLHomomorphism of L,S; ::_thesis: for g being CLHomomorphism of S,T holds g * f is CLHomomorphism of L,T
let g be CLHomomorphism of S,T; ::_thesis: g * f is CLHomomorphism of L,T
 ( f is directed-sups-preserving & g is directed-sups-preserving ) by WAYBEL16:def_1;
then A1: g * f is directed-sups-preserving by WAYBEL20:28;
 ( f is infs-preserving & g is infs-preserving ) by WAYBEL16:def_1;
then  g * f is infs-preserving by WAYBEL20:25;
hence  g * f is CLHomomorphism of L,T by A1, WAYBEL16:def_1; ::_thesis: verum
end;

theorem Th3: :: WAYBEL22:3
for L being non empty RelStr holds id L is infs-preserving
proof
let L be non empty RelStr ; ::_thesis: id L is infs-preserving
let X be Subset of L; :: according to WAYBEL_0:def_32 ::_thesis: id L preserves_inf_of X
set f = id L;
assume  ex_inf_of X,L ; :: according to WAYBEL_0:def_30 ::_thesis: ( ex_inf_of (id L) .: X,L & "/\" (((id L) .: X),L) = (id L) . ("/\" (X,L)) )
hence  ex_inf_of (id L) .: X,L by FUNCT_1:92; ::_thesis: "/\" (((id L) .: X),L) = (id L) . ("/\" (X,L))
 (id L) .: X = X by FUNCT_1:92;
hence  "/\" (((id L) .: X),L) = (id L) . ("/\" (X,L)) by FUNCT_1:18; ::_thesis: verum
end;

theorem Th4: :: WAYBEL22:4
for L being non empty RelStr holds id L is directed-sups-preserving
proof
let L be non empty RelStr ; ::_thesis: id L is directed-sups-preserving
let X be Subset of L; :: according to WAYBEL_0:def_37 ::_thesis: ( X is empty or not X is directed or id L preserves_sup_of X )
assume  ( not X is empty & X is directed ) ; ::_thesis: id L preserves_sup_of X
set f = id L;
assume  ex_sup_of X,L ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of (id L) .: X,L & "\/" (((id L) .: X),L) = (id L) . ("\/" (X,L)) )
hence  ex_sup_of (id L) .: X,L by FUNCT_1:92; ::_thesis: "\/" (((id L) .: X),L) = (id L) . ("\/" (X,L))
 (id L) .: X = X by FUNCT_1:92;
hence  "\/" (((id L) .: X),L) = (id L) . ("\/" (X,L)) by FUNCT_1:18; ::_thesis: verum
end;

theorem Th5: :: WAYBEL22:5
for L being non empty complete Poset holds id L is CLHomomorphism of L,L
proof
let L be non empty complete Poset; ::_thesis: id L is CLHomomorphism of L,L
 ( id L is directed-sups-preserving & id L is infs-preserving ) by Th3, Th4;
hence  id L is CLHomomorphism of L,L by WAYBEL16:def_1; ::_thesis: verum
end;

theorem Th6: :: WAYBEL22:6
for L being non empty upper-bounded with_infima Poset holds InclPoset (Filt L) is CLSubFrame of BoolePoset the carrier of L
proof
let L be non empty upper-bounded with_infima Poset; ::_thesis: InclPoset (Filt L) is CLSubFrame of BoolePoset the carrier of L
set cL = the carrier of L;
set BP = BoolePoset the carrier of L;
set cBP = the carrier of (BoolePoset the carrier of L);
set rBP = the InternalRel of (BoolePoset the carrier of L);
set IP = InclPoset (Filt L);
set cIP = the carrier of (InclPoset (Filt L));
set rIP = the InternalRel of (InclPoset (Filt L));
A1: InclPoset (bool the carrier of L) = RelStr(# (bool the carrier of L),(RelIncl (bool the carrier of L)) #) by YELLOW_1:def_1;
A2: InclPoset (Filt L) = RelStr(# (Filt L),(RelIncl (Filt L)) #) by YELLOW_1:def_1;
A3: BoolePoset the carrier of L = InclPoset (bool the carrier of L) by YELLOW_1:4;
A4: the carrier of (InclPoset (Filt L)) c= the carrier of (BoolePoset the carrier of L)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (InclPoset (Filt L)) or x in the carrier of (BoolePoset the carrier of L) )
assume  x in the carrier of (InclPoset (Filt L)) ; ::_thesis: x in the carrier of (BoolePoset the carrier of L)
then  ex X being Filter of L st x = X by A2;
hence  x in the carrier of (BoolePoset the carrier of L) by A3, A1; ::_thesis: verum
end;
A5: field the InternalRel of (InclPoset (Filt L)) = Filt L by A2, WELLORD2:def_1;
 the InternalRel of (InclPoset (Filt L)) c= the InternalRel of (BoolePoset the carrier of L)
proof
let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in the InternalRel of (InclPoset (Filt L)) or p in the InternalRel of (BoolePoset the carrier of L) )
assume A6: p in the InternalRel of (InclPoset (Filt L)) ; ::_thesis: p in the InternalRel of (BoolePoset the carrier of L)
then consider x, y being set  such that
A7: p = [x,y] by RELAT_1:def_1;
A8: y in field the InternalRel of (InclPoset (Filt L)) by A6, A7, RELAT_1:15;
then consider Y being Filter of L such that
A9: y = Y by A5;
A10: x in field the InternalRel of (InclPoset (Filt L)) by A6, A7, RELAT_1:15;
then consider X being Filter of L such that
A11: x = X by A5;
 X c= Y by A2, A5, A6, A7, A10, A8, A11, A9, WELLORD2:def_1;
hence  p in the InternalRel of (BoolePoset the carrier of L) by A3, A1, A7, A11, A9, WELLORD2:def_1; ::_thesis: verum
end;
then reconsider IP = InclPoset (Filt L) as SubRelStr of BoolePoset the carrier of L by A4, YELLOW_0:def_13;
now__::_thesis:_for_p_being_set_holds_
(_(_p_in_the_InternalRel_of_(InclPoset_(Filt_L))_implies_p_in_the_InternalRel_of_(BoolePoset_the_carrier_of_L)_|_2_the_carrier_of_(InclPoset_(Filt_L))_)_&_(_p_in_the_InternalRel_of_(BoolePoset_the_carrier_of_L)_|_2_the_carrier_of_(InclPoset_(Filt_L))_implies_p_in_the_InternalRel_of_(InclPoset_(Filt_L))_)_)
let p be set ; ::_thesis: ( ( p in the InternalRel of (InclPoset (Filt L)) implies p in the InternalRel of (BoolePoset the carrier of L) |_2 the carrier of (InclPoset (Filt L)) ) & ( p in the InternalRel of (BoolePoset the carrier of L) |_2 the carrier of (InclPoset (Filt L)) implies p in the InternalRel of (InclPoset (Filt L)) ) )
A12: the InternalRel of (BoolePoset the carrier of L) |_2 the carrier of (InclPoset (Filt L)) = the InternalRel of (BoolePoset the carrier of L) /\ [: the carrier of (InclPoset (Filt L)), the carrier of (InclPoset (Filt L)):] by WELLORD1:def_6;
hereby  ::_thesis: ( p in the InternalRel of (BoolePoset the carrier of L) |_2 the carrier of (InclPoset (Filt L)) implies p in the InternalRel of (InclPoset (Filt L)) )
assume A13: p in the InternalRel of (InclPoset (Filt L)) ; ::_thesis: p in the InternalRel of (BoolePoset the carrier of L) |_2 the carrier of (InclPoset (Filt L))
then consider x, y being set  such that
A14: p = [x,y] by RELAT_1:def_1;
A15: y in field the InternalRel of (InclPoset (Filt L)) by A13, A14, RELAT_1:15;
then consider Y being Filter of L such that
A16: y = Y by A5;
A17: x in field the InternalRel of (InclPoset (Filt L)) by A13, A14, RELAT_1:15;
then consider X being Filter of L such that
A18: x = X by A5;
 X c= Y by A2, A5, A13, A14, A17, A15, A18, A16, WELLORD2:def_1;
then  p in the InternalRel of (BoolePoset the carrier of L) by A3, A1, A14, A18, A16, WELLORD2:def_1;
hence  p in the InternalRel of (BoolePoset the carrier of L) |_2 the carrier of (InclPoset (Filt L)) by A12, A13, XBOOLE_0:def_4; ::_thesis: verum
end;
assume A19: p in the InternalRel of (BoolePoset the carrier of L) |_2 the carrier of (InclPoset (Filt L)) ; ::_thesis: p in the InternalRel of (InclPoset (Filt L))
then A20: p in the InternalRel of (BoolePoset the carrier of L) by A12, XBOOLE_0:def_4;
 p in [: the carrier of (InclPoset (Filt L)), the carrier of (InclPoset (Filt L)):] by A12, A19, XBOOLE_0:def_4;
then consider x, y being set  such that
A21: ( x in the carrier of (InclPoset (Filt L)) & y in the carrier of (InclPoset (Filt L)) ) and
A22: p = [x,y] by ZFMISC_1:def_2;
 ( ex X being Filter of L st x = X & ex Y being Filter of L st y = Y ) by A2, A21;
then  x c= y by A3, A1, A20, A22, WELLORD2:def_1;
hence  p in the InternalRel of (InclPoset (Filt L)) by A2, A21, A22, WELLORD2:def_1; ::_thesis: verum
end;
then  the InternalRel of (InclPoset (Filt L)) = the InternalRel of (BoolePoset the carrier of L) |_2 the carrier of (InclPoset (Filt L)) by TARSKI:1;
then reconsider IP = IP as full SubRelStr of BoolePoset the carrier of L by YELLOW_0:def_14;
A23: Filt L c= bool the carrier of L
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Filt L or x in bool the carrier of L )
assume  x in Filt L ; ::_thesis: x in bool the carrier of L
then  ex X being Filter of L st x = X ;
hence  x in bool the carrier of L ; ::_thesis: verum
end;
A24: IP is directed-sups-inheriting
proof
let X be directed Subset of IP; :: according to WAYBEL_0:def_4 ::_thesis: ( X = {} or not ex_sup_of X, BoolePoset the carrier of L or "\/" (X,(BoolePoset the carrier of L)) in the carrier of IP )
assume that
A25: X <> {} and
 ex_sup_of X, BoolePoset the carrier of L ; ::_thesis: "\/" (X,(BoolePoset the carrier of L)) in the carrier of IP
consider Y being set  such that
A26: Y in X by A25, XBOOLE_0:def_1;
reconsider F = X as Subset-Family of the carrier of L by A2, A23, XBOOLE_1:1;
A27: for P, R being Subset of L st P in F & R in F holds
ex Z being Subset of L st
( Z in F & P \/ R c= Z )
proof
let P, R be Subset of L; ::_thesis: ( P in F & R in F implies ex Z being Subset of L st
( Z in F & P \/ R c= Z ) )
assume A28: ( P in F & R in F ) ; ::_thesis: ex Z being Subset of L st
( Z in F & P \/ R c= Z )
then reconsider P9 = P, R9 = R as Element of IP ;
consider Z being Element of IP such that
A29: Z in X and
A30: ( P9 <= Z & R9 <= Z ) by A28, WAYBEL_0:def_1;
 Z in the carrier of IP by A29;
then consider Z9 being Filter of L such that
A31: Z9 = Z by A2;
take  Z9 ; ::_thesis: ( Z9 in F & P \/ R c= Z9 )
thus  Z9 in F by A29, A31; ::_thesis: P \/ R c= Z9
 ( P9 c= Z & R9 c= Z ) by A30, YELLOW_1:3;
hence  P \/ R c= Z9 by A31, XBOOLE_1:8; ::_thesis: verum
end;
reconsider X9 = X as Subset of (BoolePoset the carrier of L) by A3, A1, A2, A23, XBOOLE_1:1;
set sX = "\/" (X,(BoolePoset the carrier of L));
A32: sup X9 = union X by YELLOW_1:21;
reconsider sX = "\/" (X,(BoolePoset the carrier of L)) as Subset of L by A1, YELLOW_1:4;
A33: for X being Subset of L st X in F holds
( X is upper & X is filtered )
proof
let X be Subset of L; ::_thesis: ( X in F implies ( X is upper & X is filtered ) )
assume  X in F ; ::_thesis: ( X is upper & X is filtered )
then  X in Filt L by A2;
then  ex Y being Filter of L st X = Y ;
hence  ( X is upper & X is filtered ) ; ::_thesis: verum
end;
then  for X being Subset of L st X in F holds
X is upper ;
then A34: sX is upper by A32, WAYBEL_0:28;
 for X being Subset of L st X in F holds
X is filtered by A33;
then A35: sX is filtered by A32, A27, WAYBEL_0:47;
 Y in Filt L by A2, A26;
then  ex Z being Filter of L st Y = Z ;
then  Top L in Y by WAYBEL_4:22;
then  not sX is empty by A32, A26, TARSKI:def_4;
hence  "\/" (X,(BoolePoset the carrier of L)) in the carrier of IP by A2, A34, A35; ::_thesis: verum
end;
 IP is infs-inheriting
proof
let X be Subset of IP; :: according to YELLOW_0:def_18 ::_thesis: ( not ex_inf_of X, BoolePoset the carrier of L or "/\" (X,(BoolePoset the carrier of L)) in the carrier of IP )
assume  ex_inf_of X, BoolePoset the carrier of L ; ::_thesis: "/\" (X,(BoolePoset the carrier of L)) in the carrier of IP
set sX = "/\" (X,(BoolePoset the carrier of L));
percases ( X is empty or not X is empty ) ;
supposeA36: X is empty ; ::_thesis: "/\" (X,(BoolePoset the carrier of L)) in the carrier of IP
A37: [#] L = the carrier of L ;
"/\" (X,(BoolePoset the carrier of L)) = Top (BoolePoset the carrier of L) by A36
.= the carrier of L by YELLOW_1:19 ;
hence  "/\" (X,(BoolePoset the carrier of L)) in the carrier of IP by A2, A37; ::_thesis: verum
end;
supposeA38: not X is empty ; ::_thesis: "/\" (X,(BoolePoset the carrier of L)) in the carrier of IP
reconsider F = X as Subset-Family of the carrier of L by A2, A23, XBOOLE_1:1;
reconsider sX = "/\" (X,(BoolePoset the carrier of L)) as Subset of L by A1, YELLOW_1:4;
reconsider X9 = X as Subset of (BoolePoset the carrier of L) by A3, A1, A2, A23, XBOOLE_1:1;
A39: inf X9 = meet X by A38, YELLOW_1:20;
A40: for X being Subset of L st X in F holds
( X is upper & X is filtered )
proof
let X be Subset of L; ::_thesis: ( X in F implies ( X is upper & X is filtered ) )
assume  X in F ; ::_thesis: ( X is upper & X is filtered )
then  X in Filt L by A2;
then  ex Y being Filter of L st X = Y ;
hence  ( X is upper & X is filtered ) ; ::_thesis: verum
end;
then A41: sX is filtered by A39, YELLOW_2:39;
 for X being Subset of L st X in F holds
X is upper by A40;
then A42: sX is upper by A39, YELLOW_2:37;
 for Y being set st Y in X holds
Top L in Y
proof
let Y be set ; ::_thesis: ( Y in X implies Top L in Y )
assume  Y in X ; ::_thesis: Top L in Y
then  Y in Filt L by A2;
then  ex Z being Filter of L st Y = Z ;
hence  Top L in Y by WAYBEL_4:22; ::_thesis: verum
end;
then  not sX is empty by A38, A39, SETFAM_1:def_1;
hence  "/\" (X,(BoolePoset the carrier of L)) in the carrier of IP by A2, A42, A41; ::_thesis: verum
end;
end;
end;
hence  InclPoset (Filt L) is CLSubFrame of BoolePoset the carrier of L by A24; ::_thesis: verum
end;

registration
let L be non empty upper-bounded with_infima Poset;
cluster InclPoset (Filt L) ->  continuous ;
coherence
 InclPoset (Filt L) is continuous
proof
 InclPoset (Filt L) is CLSubFrame of BoolePoset the carrier of L by Th6;
hence  InclPoset (Filt L) is continuous by WAYBEL_5:28; ::_thesis: verum
end;
end;

registration
let L be non empty upper-bounded Poset;
cluster  ->  non empty for Element of the carrier of (InclPoset (Filt L));
coherence
 for b1 being Element of (InclPoset (Filt L)) holds not b1 is empty
proof
let x be Element of (InclPoset (Filt L)); ::_thesis: not x is empty
 InclPoset (Filt L) = RelStr(# (Filt L),(RelIncl (Filt L)) #) by YELLOW_1:def_1;
then  x in Filt L ;
then  ex X being Filter of L st x = X ;
hence  not x is empty ; ::_thesis: verum
end;
end;

begin

definition
let S be non empty complete continuous Poset;
let A be set ;
predA is_FreeGen_set_of S means :Def1: :: WAYBEL22:def 1
 for T being non empty complete continuous Poset
for f being Function of A, the carrier of T ex h being CLHomomorphism of S,T st
( h | A = f & ( for h9 being CLHomomorphism of S,T st h9 | A = f holds
h9 = h ) );
end;

:: deftheorem Def1 defines is_FreeGen_set_of WAYBEL22:def_1_:_
 for S being non empty complete continuous Poset
for A being set holds
( A is_FreeGen_set_of S iff for T being non empty complete continuous Poset
for f being Function of A, the carrier of T ex h being CLHomomorphism of S,T st
( h | A = f & ( for h9 being CLHomomorphism of S,T st h9 | A = f holds
h9 = h ) ) );

theorem Th7: :: WAYBEL22:7
for S being non empty complete continuous Poset
for A being set st A is_FreeGen_set_of S holds
A is Subset of S
proof
set T = the non empty complete continuous Poset;
let S be non empty complete continuous Poset; ::_thesis: for A being set st A is_FreeGen_set_of S holds
A is Subset of S
let A be set ; ::_thesis: ( A is_FreeGen_set_of S implies A is Subset of S )
assume A1: A is_FreeGen_set_of S ; ::_thesis: A is Subset of S
set f = the Function of A, the carrier of the non empty complete continuous Poset;
consider h being CLHomomorphism of S, the non empty complete continuous Poset such that
A2: h | A = the Function of A, the carrier of the non empty complete continuous Poset and
 for h9 being CLHomomorphism of S, the non empty complete continuous Poset st h9 | A = the Function of A, the carrier of the non empty complete continuous Poset holds
h9 = h by A1, Def1;
 dom (h | A) = (dom h) /\ A by RELAT_1:61;
hence  A is Subset of S by A2, FUNCT_2:def_1; ::_thesis: verum
end;

theorem Th8: :: WAYBEL22:8
for S being non empty complete continuous Poset
for A being set st A is_FreeGen_set_of S holds
for h9 being CLHomomorphism of S,S st h9 | A = id A holds
h9 = id S
proof
let S be non empty complete continuous Poset; ::_thesis: for A being set st A is_FreeGen_set_of S holds
for h9 being CLHomomorphism of S,S st h9 | A = id A holds
h9 = id S
let A be set ; ::_thesis: ( A is_FreeGen_set_of S implies for h9 being CLHomomorphism of S,S st h9 | A = id A holds
h9 = id S )
assume A1: A is_FreeGen_set_of S ; ::_thesis: for h9 being CLHomomorphism of S,S st h9 | A = id A holds
h9 = id S
set L = S;
A2: A is Subset of S by A1, Th7;
then A3: (id S) | A = id A by FUNCT_3:1;
 ( dom (id A) = A & rng (id A) = A ) ;
then reconsider f = id A as Function of A, the carrier of S by A2, RELSET_1:4;
consider h being CLHomomorphism of S,S such that
 h | A = f and
A4: for h9 being CLHomomorphism of S,S st h9 | A = f holds
h9 = h by A1, Def1;
A5: id S is CLHomomorphism of S,S by Th5;
let h9 be CLHomomorphism of S,S; ::_thesis: ( h9 | A = id A implies h9 = id S )
assume  h9 | A = id A ; ::_thesis: h9 = id S
hence h9 = h by A4
.= id S by A4, A5, A3 ;
::_thesis: verum
end;

begin


definition
let X be set ;
func FixedUltraFilters X ->  Subset-Family of (BoolePoset X) equals :: WAYBEL22:def 2
 {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st x = {z}  }  ;
coherence
  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st x = {z}  }  is Subset-Family of (BoolePoset X)
proof
set FUF =  {  (uparrow x) where x is Element of (BoolePoset X) : ex y being Element of X st x = {y}  }  ;
  {  (uparrow x) where x is Element of (BoolePoset X) : ex y being Element of X st x = {y}  }  c= bool the carrier of (BoolePoset X)
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in  {  (uparrow x) where x is Element of (BoolePoset X) : ex y being Element of X st x = {y}  }  or z in bool the carrier of (BoolePoset X) )
assume  z in  {  (uparrow x) where x is Element of (BoolePoset X) : ex y being Element of X st x = {y}  }  ; ::_thesis: z in bool the carrier of (BoolePoset X)
then  ex x being Element of (BoolePoset X) st
( z = uparrow x & ex y being Element of X st x = {y} ) ;
hence  z in bool the carrier of (BoolePoset X) ; ::_thesis: verum
end;
hence   {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st x = {z}  }  is Subset-Family of (BoolePoset X) ; ::_thesis: verum
end;
end;

:: deftheorem  defines FixedUltraFilters WAYBEL22:def_2_:_
 for X being set holds FixedUltraFilters X =  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st x = {z}  }  ;

theorem Th9: :: WAYBEL22:9
for X being set holds FixedUltraFilters X c= Filt (BoolePoset X)
proof
let X be set ; ::_thesis: FixedUltraFilters X c= Filt (BoolePoset X)
let F be set ; :: according to TARSKI:def_3 ::_thesis: ( not F in FixedUltraFilters X or F in Filt (BoolePoset X) )
assume  F in FixedUltraFilters X ; ::_thesis: F in Filt (BoolePoset X)
then  ex x being Element of (BoolePoset X) st
( F = uparrow x & ex y being Element of X st x = {y} ) ;
hence  F in Filt (BoolePoset X) ; ::_thesis: verum
end;

theorem Th10: :: WAYBEL22:10
for X being set holds card (FixedUltraFilters X) = card X
proof
let X be set ; ::_thesis: card (FixedUltraFilters X) = card X
set FUF =  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st x = {z}  }  ;
A1: BoolePoset X = InclPoset (bool X) by YELLOW_1:4;
A2: InclPoset (bool X) = RelStr(# (bool X),(RelIncl (bool X)) #) by YELLOW_1:def_1;
then A3: the carrier of (BoolePoset X) = bool X by YELLOW_1:4;
 X, {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st x = {z}  }  are_equipotent
proof
defpred S1[ set , set ] means  ex y being Element of X ex x being Element of (BoolePoset X) st
( x = {y} & $1 = y & $2 = uparrow x );
A4: for x being set st x in X holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in X implies ex y being set st S1[x,y] )
assume A5: x in X ; ::_thesis: ex y being set st S1[x,y]
then reconsider x9 = x as Element of X ;
reconsider bx = {x} as Element of (BoolePoset X) by A1, A2, A5, ZFMISC_1:31;
take  uparrow bx ; ::_thesis: S1[x, uparrow bx]
take  x9 ; ::_thesis: ex x being Element of (BoolePoset X) st
( x = {x9} & x = x9 & uparrow bx = uparrow x )
take  bx ; ::_thesis: ( bx = {x9} & x = x9 & uparrow bx = uparrow bx )
thus  ( bx = {x9} & x = x9 & uparrow bx = uparrow bx ) ; ::_thesis: verum
end;
consider f being Function such that
A6: ( dom f = X & ( for x being set st x in X holds
S1[x,f . x] ) ) from CLASSES1:sch_1(A4);
take  f ; :: according to WELLORD2:def_4 ::_thesis: ( f is one-to-one & dom f = X & rng f =  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st x = {z}  }  )
thus  f is one-to-one ::_thesis: ( dom f = X & rng f =  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st x = {z}  }  )
proof
let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom f or not x2 in dom f or not f . x1 = f . x2 or x1 = x2 )
assume that
A7: x1 in dom f and
A8: x2 in dom f and
A9: f . x1 = f . x2 ; ::_thesis: x1 = x2
consider x29 being Element of X, bx2 being Element of (BoolePoset X) such that
A10: ( bx2 = {x29} & x2 = x29 ) and
A11: f . x2 = uparrow bx2 by A6, A8;
consider x19 being Element of X, bx1 being Element of (BoolePoset X) such that
A12: ( bx1 = {x19} & x1 = x19 ) and
A13: f . x1 = uparrow bx1 by A6, A7;
 bx1 = bx2 by A9, A13, A11, WAYBEL_0:20;
hence  x1 = x2 by A12, A10, ZFMISC_1:3; ::_thesis: verum
end;
thus  dom f = X by A6; ::_thesis: rng f =  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st x = {z}  }
now__::_thesis:_for_z_being_set_holds_
(_(_z_in_rng_f_implies_z_in__{__(uparrow_x)_where_x_is_Element_of_(BoolePoset_X)_:_ex_z_being_Element_of_X_st_x_=_{z}__}__)_&_(_z_in__{__(uparrow_x)_where_x_is_Element_of_(BoolePoset_X)_:_ex_z_being_Element_of_X_st_x_=_{z}__}__implies_z_in_rng_f_)_)
let z be set ; ::_thesis: ( ( z in rng f implies z in  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st x = {z}  }  ) & ( z in  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st x = {z}  }  implies z in rng f ) )
hereby  ::_thesis: ( z in  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st x = {z}  }  implies z in rng f )
assume  z in rng f ; ::_thesis: z in  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st x = {z}  }
then consider x1 being set  such that
A14: x1 in dom f and
A15: z = f . x1 by FUNCT_1:def_3;
 ex x19 being Element of X ex bx1 being Element of (BoolePoset X) st
( bx1 = {x19} & x1 = x19 & f . x1 = uparrow bx1 ) by A6, A14;
hence  z in  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st x = {z}  }  by A15; ::_thesis: verum
end;
assume  z in  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st x = {z}  }  ; ::_thesis: z in rng f
then consider bx being Element of (BoolePoset X) such that
A16: z = uparrow bx and
A17: ex y being Element of X st bx = {y} ;
consider y being Element of X such that
A18: bx = {y} by A17;
A19: y in X by A3, A18, ZFMISC_1:31;
then  ex x19 being Element of X ex bx1 being Element of (BoolePoset X) st
( bx1 = {x19} & y = x19 & f . y = uparrow bx1 ) by A6;
hence  z in rng f by A6, A16, A18, A19, FUNCT_1:def_3; ::_thesis: verum
end;
hence  rng f =  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st x = {z}  }  by TARSKI:1; ::_thesis: verum
end;
hence  card (FixedUltraFilters X) = card X by CARD_1:5; ::_thesis: verum
end;

theorem Th11: :: WAYBEL22:11
for X being set
for F being Filter of (BoolePoset X) holds F = "\/" ( {  ("/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F  }  ,(InclPoset (Filt (BoolePoset X))))
proof
let X be set ; ::_thesis: for F being Filter of (BoolePoset X) holds F = "\/" ( {  ("/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F  }  ,(InclPoset (Filt (BoolePoset X))))
let F be Filter of (BoolePoset X); ::_thesis: F = "\/" ( {  ("/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F  }  ,(InclPoset (Filt (BoolePoset X))))
set BP = BoolePoset X;
set IP = InclPoset (Filt (BoolePoset X));
set cIP = the carrier of (InclPoset (Filt (BoolePoset X)));
set Xs =  {  ("/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F  }  ;
set RS = "\/" ( {  ("/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F  }  ,(InclPoset (Filt (BoolePoset X))));
A1: InclPoset (Filt (BoolePoset X)) = RelStr(# (Filt (BoolePoset X)),(RelIncl (Filt (BoolePoset X))) #) by YELLOW_1:def_1;
 F in Filt (BoolePoset X) ;
then reconsider F9 = F as Element of (InclPoset (Filt (BoolePoset X))) by A1;
A2:  {  ("/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F  }  c= the carrier of (InclPoset (Filt (BoolePoset X)))
proof
let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in  {  ("/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F  }  or p in the carrier of (InclPoset (Filt (BoolePoset X))) )
assume  p in  {  ("/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F  }  ; ::_thesis: p in the carrier of (InclPoset (Filt (BoolePoset X)))
then  ex YY being Subset of X st
( p = "/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in YY )  }  ,(InclPoset (Filt (BoolePoset X)))) & YY in F ) ;
hence  p in the carrier of (InclPoset (Filt (BoolePoset X))) ; ::_thesis: verum
end;
A3: the carrier of (BoolePoset X) = the carrier of (LattPOSet (BooleLatt X)) by YELLOW_1:def_2
.= bool X by LATTICE3:def_1 ;
now__::_thesis:_not__{__("/\"_(_{__(uparrow_x)_where_x_is_Element_of_(BoolePoset_X)_:_ex_z_being_Element_of_X_st_
(_x_=_{z}_&_z_in_Y_)__}__,(InclPoset_(Filt_(BoolePoset_X)))))_where_Y_is_Subset_of_X_:_Y_in_F__}__is_empty
consider YY being set  such that
A4: YY in F by XBOOLE_0:def_1;
 "/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in YY )  }  ,(InclPoset (Filt (BoolePoset X)))) in  {  ("/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F  }  by A3, A4;
hence  not  {  ("/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F  }  is empty ; ::_thesis: verum
end;
then reconsider Xs9 =  {  ("/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F  }  as non empty Subset of (InclPoset (Filt (BoolePoset X))) by A2;
A5: ex_sup_of Xs9, InclPoset (Filt (BoolePoset X)) by YELLOW_0:17;
 F c= "\/" ( {  ("/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F  }  ,(InclPoset (Filt (BoolePoset X))))
proof
let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in F or p in "\/" ( {  ("/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F  }  ,(InclPoset (Filt (BoolePoset X)))) )
assume A6: p in F ; ::_thesis: p in "\/" ( {  ("/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F  }  ,(InclPoset (Filt (BoolePoset X))))
then reconsider Y = p as Element of F ;
set Xsi =  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ;
A7: "/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,(InclPoset (Filt (BoolePoset X)))) in  {  ("/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F  }  by A3;
percases (  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  is empty or not  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  is empty ) ;
supposeA8:  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  is empty ; ::_thesis: p in "\/" ( {  ("/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F  }  ,(InclPoset (Filt (BoolePoset X))))
A9: p in the carrier of (BoolePoset X) by A6;
 Xs9 is_<=_than "\/" ( {  ("/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F  }  ,(InclPoset (Filt (BoolePoset X)))) by A5, YELLOW_0:def_9;
then A10: "/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,(InclPoset (Filt (BoolePoset X)))) <= "\/" ( {  ("/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F  }  ,(InclPoset (Filt (BoolePoset X)))) by A7, LATTICE3:def_9;
"/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,(InclPoset (Filt (BoolePoset X)))) = Top (InclPoset (Filt (BoolePoset X))) by A8
.= bool X by WAYBEL16:15 ;
then  bool X c= "\/" ( {  ("/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F  }  ,(InclPoset (Filt (BoolePoset X)))) by A10, YELLOW_1:3;
hence  p in "\/" ( {  ("/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F  }  ,(InclPoset (Filt (BoolePoset X)))) by A3, A9; ::_thesis: verum
end;
supposeA11: not  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  is empty ; ::_thesis: p in "\/" ( {  ("/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F  }  ,(InclPoset (Filt (BoolePoset X))))
  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  c= the carrier of (InclPoset (Filt (BoolePoset X)))
proof
let r be set ; :: according to TARSKI:def_3 ::_thesis: ( not r in  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  or r in the carrier of (InclPoset (Filt (BoolePoset X))) )
assume  r in  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ; ::_thesis: r in the carrier of (InclPoset (Filt (BoolePoset X)))
then  ex xz being Element of (BoolePoset X) st
( r = uparrow xz & ex z being Element of X st
( xz = {z} & z in Y ) ) ;
hence  r in the carrier of (InclPoset (Filt (BoolePoset X))) by A1; ::_thesis: verum
end;
then reconsider Xsi =  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  as non empty Subset of (InclPoset (Filt (BoolePoset X))) by A11;
 for yy being set st yy in Xsi holds
Y in yy
proof
reconsider Y9 = Y as Element of (BoolePoset X) ;
let yy be set ; ::_thesis: ( yy in Xsi implies Y in yy )
assume  yy in Xsi ; ::_thesis: Y in yy
then consider r being Element of (BoolePoset X) such that
A12: yy = uparrow r and
A13: ex z being Element of X st
( r = {z} & z in Y ) ;
 r c= Y by A13, ZFMISC_1:31;
then  r <= Y9 by YELLOW_1:2;
hence  Y in yy by A12, WAYBEL_0:18; ::_thesis: verum
end;
then  ( "/\" (Xsi,(InclPoset (Filt (BoolePoset X)))) = meet Xsi & Y in meet Xsi ) by SETFAM_1:def_1, WAYBEL16:10;
then A14: p in union  {  ("/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F  }  by A7, TARSKI:def_4;
 union Xs9 c= "\/" ( {  ("/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F  }  ,(InclPoset (Filt (BoolePoset X)))) by WAYBEL16:17, YELLOW_0:17;
hence  p in "\/" ( {  ("/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F  }  ,(InclPoset (Filt (BoolePoset X)))) by A14; ::_thesis: verum
end;
end;
end;
then A15: F9 <= "\/" ( {  ("/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F  }  ,(InclPoset (Filt (BoolePoset X)))) by YELLOW_1:3;
  {  ("/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F  }  is_<=_than F9
proof
let b be Element of (InclPoset (Filt (BoolePoset X))); :: according to LATTICE3:def_9 ::_thesis: ( not b in  {  ("/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F  }  or b <= F9 )
assume  b in  {  ("/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F  }  ; ::_thesis: b <= F9
then consider Y being Subset of X such that
A16: b = "/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,(InclPoset (Filt (BoolePoset X)))) and
A17: Y in F ;
reconsider Y9 = Y as Element of F by A17;
set Xsi =  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ;
percases ( Y is empty or not Y is empty ) ;
supposeA18: Y is empty ; ::_thesis: b <= F9
now__::_thesis:__{__(uparrow_x)_where_x_is_Element_of_(BoolePoset_X)_:_ex_z_being_Element_of_X_st_
(_x_=_{z}_&_z_in_Y_)__}__is_empty
assume  not  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  is empty ; ::_thesis: contradiction
then consider p being set  such that
A19: p in  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  by XBOOLE_0:def_1;
 ex x being Element of (BoolePoset X) st
( p = uparrow x & ex z being Element of X st
( x = {z} & z in Y ) ) by A19;
hence  contradiction by A18; ::_thesis: verum
end;
then A20: "/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,(InclPoset (Filt (BoolePoset X)))) = Top (InclPoset (Filt (BoolePoset X)))
.= bool X by WAYBEL16:15 ;
 Bottom (BoolePoset X) = {} by YELLOW_1:18;
then  uparrow (Bottom (BoolePoset X)) c= F by A17, A18, WAYBEL11:42;
then  bool X c= F by A3, WAYBEL14:10;
hence  b <= F9 by A3, A16, A20, XBOOLE_0:def_10; ::_thesis: verum
end;
supposeA21: not Y is empty ; ::_thesis: b <= F9
A22: now__::_thesis:_not__{__(uparrow_x)_where_x_is_Element_of_(BoolePoset_X)_:_ex_z_being_Element_of_X_st_
(_x_=_{z}_&_z_in_Y_)__}__is_empty
consider z being set  such that
A23: z in Y by A21, XBOOLE_0:def_1;
reconsider z = z as Element of X by A23;
reconsider x = {z} as Element of (BoolePoset X) by A3, A23, ZFMISC_1:31;
 uparrow x in  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  by A23;
hence  not  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  is empty ; ::_thesis: verum
end;
  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  c= the carrier of (InclPoset (Filt (BoolePoset X)))
proof
let r be set ; :: according to TARSKI:def_3 ::_thesis: ( not r in  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  or r in the carrier of (InclPoset (Filt (BoolePoset X))) )
assume  r in  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ; ::_thesis: r in the carrier of (InclPoset (Filt (BoolePoset X)))
then  ex xz being Element of (BoolePoset X) st
( r = uparrow xz & ex z being Element of X st
( xz = {z} & z in Y ) ) ;
hence  r in the carrier of (InclPoset (Filt (BoolePoset X))) by A1; ::_thesis: verum
end;
then reconsider Xsi =  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  as non empty Subset of (InclPoset (Filt (BoolePoset X))) by A22;
A24: "/\" (Xsi,(InclPoset (Filt (BoolePoset X)))) = meet Xsi by WAYBEL16:10;
 b c= F9
proof
let yy be set ; :: according to TARSKI:def_3 ::_thesis: ( not yy in b or yy in F9 )
 b in Filt (BoolePoset X) by A1;
then consider bf being Filter of (BoolePoset X) such that
A25: b = bf ;
assume A26: yy in b ; ::_thesis: yy in F9
then reconsider yy9 = yy as Element of bf by A25;
reconsider yy9 = yy9 as Element of (BoolePoset X) ;
 Y c= yy9
proof
let zz be set ; :: according to TARSKI:def_3 ::_thesis: ( not zz in Y or zz in yy9 )
assume A27: zz in Y ; ::_thesis: zz in yy9
then reconsider z = zz as Element of X ;
reconsider xz = {z} as Element of (BoolePoset X) by A3, A27, ZFMISC_1:31;
 uparrow xz in Xsi by A27;
then  yy in uparrow xz by A16, A24, A26, SETFAM_1:def_1;
then  xz <= yy9 by WAYBEL_0:18;
then  {z} c= yy by YELLOW_1:2;
hence  zz in yy9 by ZFMISC_1:31; ::_thesis: verum
end;
then  Y9 <= yy9 by YELLOW_1:2;
then  ( uparrow Y9 c= F9 & yy in uparrow Y9 ) by WAYBEL11:42, WAYBEL_0:18;
hence  yy in F9 ; ::_thesis: verum
end;
hence  b <= F9 by YELLOW_1:3; ::_thesis: verum
end;
end;
end;
then  "\/" ( {  ("/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F  }  ,(InclPoset (Filt (BoolePoset X)))) <= F9 by A5, YELLOW_0:def_9;
hence  F = "\/" ( {  ("/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F  }  ,(InclPoset (Filt (BoolePoset X)))) by A15, YELLOW_0:def_3; ::_thesis: verum
end;

definition
let X be set ;
let L be non empty complete continuous Poset;
let f be Function of (FixedUltraFilters X), the carrier of L;
funcf -extension_to_hom  ->  Function of (InclPoset (Filt (BoolePoset X))),L means :Def3: :: WAYBEL22:def 3
 for Fi being Element of (InclPoset (Filt (BoolePoset X))) holds it . Fi = "\/" ( {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in Fi  }  ,L);
existence
 ex b1 being Function of (InclPoset (Filt (BoolePoset X))),L st
for Fi being Element of (InclPoset (Filt (BoolePoset X))) holds b1 . Fi = "\/" ( {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in Fi  }  ,L)
proof
set IP = InclPoset (Filt (BoolePoset X));
deffunc H1( Element of (InclPoset (Filt (BoolePoset X)))) ->  Element of the carrier of L = "\/" ( {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in $1  }  ,L);
consider F being Function of the carrier of (InclPoset (Filt (BoolePoset X))), the carrier of L such that
A1: for Fi being Element of (InclPoset (Filt (BoolePoset X))) holds F . Fi = H1(Fi) from FUNCT_2:sch_4();
reconsider F = F as Function of (InclPoset (Filt (BoolePoset X))),L ;
take  F ; ::_thesis: for Fi being Element of (InclPoset (Filt (BoolePoset X))) holds F . Fi = "\/" ( {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in Fi  }  ,L)
thus  for Fi being Element of (InclPoset (Filt (BoolePoset X))) holds F . Fi = "\/" ( {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in Fi  }  ,L) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of (InclPoset (Filt (BoolePoset X))),L st ( for Fi being Element of (InclPoset (Filt (BoolePoset X))) holds b1 . Fi = "\/" ( {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in Fi  }  ,L) ) & ( for Fi being Element of (InclPoset (Filt (BoolePoset X))) holds b2 . Fi = "\/" ( {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in Fi  }  ,L) ) holds
b1 = b2
proof
set IP = InclPoset (Filt (BoolePoset X));
let it1, it2 be Function of (InclPoset (Filt (BoolePoset X))),L; ::_thesis: ( ( for Fi being Element of (InclPoset (Filt (BoolePoset X))) holds it1 . Fi = "\/" ( {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in Fi  }  ,L) ) & ( for Fi being Element of (InclPoset (Filt (BoolePoset X))) holds it2 . Fi = "\/" ( {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in Fi  }  ,L) ) implies it1 = it2 )
assume that
A2: for Fi being Element of (InclPoset (Filt (BoolePoset X))) holds it1 . Fi = "\/" ( {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in Fi  }  ,L) and
A3: for Fi being Element of (InclPoset (Filt (BoolePoset X))) holds it2 . Fi = "\/" ( {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in Fi  }  ,L) ; ::_thesis: it1 = it2
reconsider it29 = it2 as Function of the carrier of (InclPoset (Filt (BoolePoset X))), the carrier of L ;
reconsider it19 = it1 as Function of the carrier of (InclPoset (Filt (BoolePoset X))), the carrier of L ;
now__::_thesis:_for_Fi_being_Element_of_(InclPoset_(Filt_(BoolePoset_X)))_holds_it19_._Fi_=_it29_._Fi
let Fi be Element of (InclPoset (Filt (BoolePoset X))); ::_thesis: it19 . Fi = it29 . Fi
thus it19 . Fi = "\/" ( {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in Fi  }  ,L) by A2
.= it29 . Fi by A3 ; ::_thesis: verum
end;
hence  it1 = it2 by FUNCT_2:63; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines -extension_to_hom WAYBEL22:def_3_:_
 for X being set
for L being non empty complete continuous Poset
for f being Function of (FixedUltraFilters X), the carrier of L
for b4 being Function of (InclPoset (Filt (BoolePoset X))),L holds
( b4 = f -extension_to_hom iff for Fi being Element of (InclPoset (Filt (BoolePoset X))) holds b4 . Fi = "\/" ( {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in Fi  }  ,L) );

theorem :: WAYBEL22:12
for X being set
for L being non empty complete continuous Poset
for f being Function of (FixedUltraFilters X), the carrier of L holds f -extension_to_hom is monotone
proof
let X be set ; ::_thesis: for L being non empty complete continuous Poset
for f being Function of (FixedUltraFilters X), the carrier of L holds f -extension_to_hom is monotone
let L be non empty complete continuous Poset; ::_thesis: for f being Function of (FixedUltraFilters X), the carrier of L holds f -extension_to_hom is monotone
let f be Function of (FixedUltraFilters X), the carrier of L; ::_thesis: f -extension_to_hom is monotone
let F1, F2 be Element of (InclPoset (Filt (BoolePoset X))); :: according to ORDERS_3:def_5 ::_thesis: ( not F1 <= F2 or for b1, b2 being Element of the carrier of L holds
( not b1 = (f -extension_to_hom) . F1 or not b2 = (f -extension_to_hom) . F2 or b1 <= b2 ) )
set F = f -extension_to_hom ;
set F1s =  {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in F1  }  ;
set F2s =  {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in F2  }  ;
A1: ( ex_sup_of  {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in F1  }  ,L & ex_sup_of  {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in F2  }  ,L ) by YELLOW_0:17;
A2: (f -extension_to_hom) . F1 = "\/" ( {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in F1  }  ,L) by Def3;
assume  F1 <= F2 ; ::_thesis: for b1, b2 being Element of the carrier of L holds
( not b1 = (f -extension_to_hom) . F1 or not b2 = (f -extension_to_hom) . F2 or b1 <= b2 )
then A3: F1 c= F2 by YELLOW_1:3;
A4:  {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in F1  }  c=  {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in F2  }
proof
let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in  {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in F1  }  or s in  {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in F2  }  )
assume  s in  {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in F1  }  ; ::_thesis: s in  {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in F2  }
then  ex Y being Subset of X st
( s = "/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L) & Y in F1 ) ;
hence  s in  {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in F2  }  by A3; ::_thesis: verum
end;
A5: (f -extension_to_hom) . F2 = "\/" ( {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in F2  }  ,L) by Def3;
let FF1, FF2 be Element of L; ::_thesis: ( not FF1 = (f -extension_to_hom) . F1 or not FF2 = (f -extension_to_hom) . F2 or FF1 <= FF2 )
assume  ( FF1 = (f -extension_to_hom) . F1 & FF2 = (f -extension_to_hom) . F2 ) ; ::_thesis: FF1 <= FF2
hence  FF1 <= FF2 by A2, A5, A1, A4, YELLOW_0:34; ::_thesis: verum
end;

theorem Th13: :: WAYBEL22:13
for X being set
for L being non empty complete continuous Poset
for f being Function of (FixedUltraFilters X), the carrier of L holds (f -extension_to_hom) . (Top (InclPoset (Filt (BoolePoset X)))) = Top L
proof
let X be set ; ::_thesis: for L being non empty complete continuous Poset
for f being Function of (FixedUltraFilters X), the carrier of L holds (f -extension_to_hom) . (Top (InclPoset (Filt (BoolePoset X)))) = Top L
let L be non empty complete continuous Poset; ::_thesis: for f being Function of (FixedUltraFilters X), the carrier of L holds (f -extension_to_hom) . (Top (InclPoset (Filt (BoolePoset X)))) = Top L
let f be Function of (FixedUltraFilters X), the carrier of L; ::_thesis: (f -extension_to_hom) . (Top (InclPoset (Filt (BoolePoset X)))) = Top L
set IP = InclPoset (Filt (BoolePoset X));
set F = f -extension_to_hom ;
reconsider T = Top (InclPoset (Filt (BoolePoset X))) as Element of (InclPoset (Filt (BoolePoset X))) ;
reconsider E = {} as Subset of X by XBOOLE_1:2;
set Z =  {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in T  }  ;
A1:  {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in E )  }  = {}
proof
assume  not  {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in E )  }  = {} ; ::_thesis: contradiction
then consider r being set  such that
A2: r in  {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in E )  }  by XBOOLE_0:def_1;
 ex x being Element of (BoolePoset X) st
( r = f . (uparrow x) & ex z being Element of X st
( x = {z} & z in E ) ) by A2;
hence  contradiction ; ::_thesis: verum
end;
A3: (f -extension_to_hom) . T = "\/" ( {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in T  }  ,L) by Def3;
 T = bool X by WAYBEL16:15;
then A4: "/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in E )  }  ,L) in  {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in T  }  ;
  {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in T  }  is_<=_than "\/" ( {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in T  }  ,L) by YELLOW_0:32;
then  Top L <= "\/" ( {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in T  }  ,L) by A4, A1, LATTICE3:def_9;
hence  (f -extension_to_hom) . (Top (InclPoset (Filt (BoolePoset X)))) = Top L by A3, WAYBEL15:3; ::_thesis: verum
end;

registration
let X be set ;
let L be non empty complete continuous Poset;
let f be Function of (FixedUltraFilters X), the carrier of L;
clusterf -extension_to_hom  ->  directed-sups-preserving ;
coherence
 f -extension_to_hom is directed-sups-preserving
proof
set F = f -extension_to_hom ;
set IP = InclPoset (Filt (BoolePoset X));
let Fs be Subset of (InclPoset (Filt (BoolePoset X))); :: according to WAYBEL_0:def_37 ::_thesis: ( Fs is empty or not Fs is directed or f -extension_to_hom preserves_sup_of Fs )
assume A1: ( not Fs is empty & Fs is directed ) ; ::_thesis: f -extension_to_hom preserves_sup_of Fs
reconsider Fs9 = Fs as non empty Subset of (InclPoset (Filt (BoolePoset X))) by A1;
set FFsU =  {   {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in YY  }  where YY is Element of Fs9 : verum  }  ;
reconsider sFs = sup Fs as Element of (InclPoset (Filt (BoolePoset X))) ;
set FFs =  {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in sFs  }  ;
A2: sup Fs = union Fs by A1, Th1;
now__::_thesis:_for_p_being_set_holds_
(_(_p_in__{__("/\"_(_{__(f_._(uparrow_x))_where_x_is_Element_of_(BoolePoset_X)_:_ex_z_being_Element_of_X_st_
(_x_=_{z}_&_z_in_Y_)__}__,L))_where_Y_is_Subset_of_X_:_Y_in_sFs__}__implies_p_in_union__{___{__("/\"_(_{__(f_._(uparrow_x))_where_x_is_Element_of_(BoolePoset_X)_:_ex_z_being_Element_of_X_st_
(_x_=_{z}_&_z_in_Y_)__}__,L))_where_Y_is_Subset_of_X_:_Y_in_YY__}__where_YY_is_Element_of_Fs9_:_verum__}__)_&_(_p_in_union__{___{__("/\"_(_{__(f_._(uparrow_x))_where_x_is_Element_of_(BoolePoset_X)_:_ex_z_being_Element_of_X_st_
(_x_=_{z}_&_z_in_Y_)__}__,L))_where_Y_is_Subset_of_X_:_Y_in_YY__}__where_YY_is_Element_of_Fs9_:_verum__}__implies_p_in__{__("/\"_(_{__(f_._(uparrow_x))_where_x_is_Element_of_(BoolePoset_X)_:_ex_z_being_Element_of_X_st_
(_x_=_{z}_&_z_in_Y_)__}__,L))_where_Y_is_Subset_of_X_:_Y_in_sFs__}__)_)
let p be set ; ::_thesis: ( ( p in  {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in sFs  }  implies p in union  {   {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in YY  }  where YY is Element of Fs9 : verum  }  ) & ( p in union  {   {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in YY  }  where YY is Element of Fs9 : verum  }  implies p in  {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in sFs  }  ) )
hereby  ::_thesis: ( p in union  {   {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in YY  }  where YY is Element of Fs9 : verum  }  implies p in  {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in sFs  }  )
assume  p in  {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in sFs  }  ; ::_thesis: p in union  {   {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in YY  }  where YY is Element of Fs9 : verum  }
then consider Y being Subset of X such that
A3: p = "/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L) and
A4: Y in sFs ;
consider YY being set  such that
A5: Y in YY and
A6: YY in Fs by A2, A4, TARSKI:def_4;
A7:  {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y1 )  }  ,L)) where Y1 is Subset of X : Y1 in YY  }  in  {   {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in YY  }  where YY is Element of Fs9 : verum  }  by A6;
 p in  {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y1 )  }  ,L)) where Y1 is Subset of X : Y1 in YY  }  by A3, A5;
hence  p in union  {   {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in YY  }  where YY is Element of Fs9 : verum  }  by A7, TARSKI:def_4; ::_thesis: verum
end;
assume  p in union  {   {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in YY  }  where YY is Element of Fs9 : verum  }  ; ::_thesis: p in  {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in sFs  }
then consider r being set  such that
A8: p in r and
A9: r in  {   {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in YY  }  where YY is Element of Fs9 : verum  }  by TARSKI:def_4;
consider YY being Element of Fs9 such that
A10: r =  {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in YY  }  by A9;
consider Y being Subset of X such that
A11: p = "/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L) and
A12: Y in YY by A8, A10;
 Y in sFs by A2, A12, TARSKI:def_4;
hence  p in  {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in sFs  }  by A11; ::_thesis: verum
end;
then A13:  {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in sFs  }  = union  {   {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in YY  }  where YY is Element of Fs9 : verum  }  by TARSKI:1;
set Zs =  {  (sup Z) where Z is Subset of L : Z in  {   {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in YY  }  where YY is Element of Fs9 : verum  }   }  ;
assume  ex_sup_of Fs, InclPoset (Filt (BoolePoset X)) ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of (f -extension_to_hom) .: Fs,L & "\/" (((f -extension_to_hom) .: Fs),L) = (f -extension_to_hom) . ("\/" (Fs,(InclPoset (Filt (BoolePoset X))))) )
thus  ex_sup_of (f -extension_to_hom) .: Fs,L by YELLOW_0:17; ::_thesis: "\/" (((f -extension_to_hom) .: Fs),L) = (f -extension_to_hom) . ("\/" (Fs,(InclPoset (Filt (BoolePoset X)))))
  {   {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in YY  }  where YY is Element of Fs9 : verum  }  c= bool the carrier of L
proof
let r be set ; :: according to TARSKI:def_3 ::_thesis: ( not r in  {   {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in YY  }  where YY is Element of Fs9 : verum  }  or r in bool the carrier of L )
assume  r in  {   {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in YY  }  where YY is Element of Fs9 : verum  }  ; ::_thesis: r in bool the carrier of L
then consider YY being Element of Fs9 such that
A14: r =  {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in YY  }  ;
 r c= the carrier of L
proof
let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in r or s in the carrier of L )
assume  s in r ; ::_thesis: s in the carrier of L
then  ex Y being Subset of X st
( s = "/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L) & Y in YY ) by A14;
hence  s in the carrier of L ; ::_thesis: verum
end;
hence  r in bool the carrier of L ; ::_thesis: verum
end;
then A15: "\/" ((union  {   {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in YY  }  where YY is Element of Fs9 : verum  }  ),L) = "\/" ( {  (sup Z) where Z is Subset of L : Z in  {   {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in YY  }  where YY is Element of Fs9 : verum  }   }  ,L) by Lm2;
A16: now__::_thesis:_for_r_being_set_holds_
(_(_r_in_(f_-extension_to_hom)_.:_Fs_implies_r_in__{__(sup_Z)_where_Z_is_Subset_of_L_:_Z_in__{___{__("/\"_(_{__(f_._(uparrow_x))_where_x_is_Element_of_(BoolePoset_X)_:_ex_z_being_Element_of_X_st_
(_x_=_{z}_&_z_in_Y_)__}__,L))_where_Y_is_Subset_of_X_:_Y_in_YY__}__where_YY_is_Element_of_Fs9_:_verum__}___}__)_&_(_r_in__{__(sup_Z)_where_Z_is_Subset_of_L_:_Z_in__{___{__("/\"_(_{__(f_._(uparrow_x))_where_x_is_Element_of_(BoolePoset_X)_:_ex_z_being_Element_of_X_st_
(_x_=_{z}_&_z_in_Y_)__}__,L))_where_Y_is_Subset_of_X_:_Y_in_YY__}__where_YY_is_Element_of_Fs9_:_verum__}___}__implies_r_in_(f_-extension_to_hom)_.:_Fs_)_)
let r be set ; ::_thesis: ( ( r in (f -extension_to_hom) .: Fs implies r in  {  (sup Z) where Z is Subset of L : Z in  {   {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in YY  }  where YY is Element of Fs9 : verum  }   }  ) & ( r in  {  (sup Z) where Z is Subset of L : Z in  {   {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in YY  }  where YY is Element of Fs9 : verum  }   }  implies r in (f -extension_to_hom) .: Fs ) )
hereby  ::_thesis: ( r in  {  (sup Z) where Z is Subset of L : Z in  {   {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in YY  }  where YY is Element of Fs9 : verum  }   }  implies r in (f -extension_to_hom) .: Fs )
assume  r in (f -extension_to_hom) .: Fs ; ::_thesis: r in  {  (sup Z) where Z is Subset of L : Z in  {   {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in YY  }  where YY is Element of Fs9 : verum  }   }
then consider YY being set  such that
A17: YY in the carrier of (InclPoset (Filt (BoolePoset X))) and
A18: YY in Fs and
A19: (f -extension_to_hom) . YY = r by FUNCT_2:64;
reconsider YY = YY as Element of Fs by A18;
reconsider YY9 = YY as Element of (InclPoset (Filt (BoolePoset X))) by A17;
set Zi =  {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in YY9  }  ;
  {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in YY9  }  c= the carrier of L
proof
let t be set ; :: according to TARSKI:def_3 ::_thesis: ( not t in  {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in YY9  }  or t in the carrier of L )
assume  t in  {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in YY9  }  ; ::_thesis: t in the carrier of L
then  ex Y being Subset of X st
( t = "/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L) & Y in YY9 ) ;
hence  t in the carrier of L ; ::_thesis: verum
end;
then reconsider Zi =  {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in YY9  }  as Subset of L ;
A20: Zi in  {   {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in YY  }  where YY is Element of Fs9 : verum  }  ;
 (f -extension_to_hom) . YY9 = "\/" ( {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in YY9  }  ,L) by Def3;
hence  r in  {  (sup Z) where Z is Subset of L : Z in  {   {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in YY  }  where YY is Element of Fs9 : verum  }   }  by A19, A20; ::_thesis: verum
end;
assume  r in  {  (sup Z) where Z is Subset of L : Z in  {   {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in YY  }  where YY is Element of Fs9 : verum  }   }  ; ::_thesis: r in (f -extension_to_hom) .: Fs
then consider Z being Subset of L such that
A21: r = sup Z and
A22: Z in  {   {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in YY  }  where YY is Element of Fs9 : verum  }  ;
consider YY being Element of Fs such that
A23: Z =  {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in YY  }  by A22;
reconsider YY = YY as Element of Fs9 ;
reconsider YY9 = YY as Element of (InclPoset (Filt (BoolePoset X))) ;
 (f -extension_to_hom) . YY9 = "\/" ( {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in YY9  }  ,L) by Def3;
hence  r in (f -extension_to_hom) .: Fs by A21, A23, FUNCT_2:35; ::_thesis: verum
end;
 (f -extension_to_hom) . sFs = "\/" ( {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in sFs  }  ,L) by Def3;
hence  "\/" (((f -extension_to_hom) .: Fs),L) = (f -extension_to_hom) . ("\/" (Fs,(InclPoset (Filt (BoolePoset X))))) by A15, A13, A16, TARSKI:1; ::_thesis: verum
end;
end;

registration
let X be set ;
let L be non empty complete continuous Poset;
let f be Function of (FixedUltraFilters X), the carrier of L;
clusterf -extension_to_hom  ->  infs-preserving ;
coherence
 f -extension_to_hom is infs-preserving
proof
set FUF = FixedUltraFilters X;
set cL = the carrier of L;
set F = f -extension_to_hom ;
set BP = BoolePoset X;
set IP = InclPoset (Filt (BoolePoset X));
set cIP = the carrier of (InclPoset (Filt (BoolePoset X)));
A1: InclPoset (Filt (BoolePoset X)) = RelStr(# (Filt (BoolePoset X)),(RelIncl (Filt (BoolePoset X))) #) by YELLOW_1:def_1;
let Fs be Subset of (InclPoset (Filt (BoolePoset X))); :: according to WAYBEL_0:def_32 ::_thesis: f -extension_to_hom preserves_inf_of Fs
assume  ex_inf_of Fs, InclPoset (Filt (BoolePoset X)) ; :: according to WAYBEL_0:def_30 ::_thesis: ( ex_inf_of (f -extension_to_hom) .: Fs,L & "/\" (((f -extension_to_hom) .: Fs),L) = (f -extension_to_hom) . ("/\" (Fs,(InclPoset (Filt (BoolePoset X))))) )
thus  ex_inf_of (f -extension_to_hom) .: Fs,L by YELLOW_0:17; ::_thesis: "/\" (((f -extension_to_hom) .: Fs),L) = (f -extension_to_hom) . ("/\" (Fs,(InclPoset (Filt (BoolePoset X)))))
A2: BoolePoset X = InclPoset (bool X) by YELLOW_1:4;
A3: InclPoset (bool X) = RelStr(# (bool X),(RelIncl (bool X)) #) by YELLOW_1:def_1;
then A4: the carrier of (BoolePoset X) = bool X by YELLOW_1:4;
percases ( Fs is empty or not Fs is empty ) ;
suppose Fs is empty ; ::_thesis: "/\" (((f -extension_to_hom) .: Fs),L) = (f -extension_to_hom) . ("/\" (Fs,(InclPoset (Filt (BoolePoset X)))))
then  ( "/\" (((f -extension_to_hom) .: Fs),L) = Top L & "/\" (Fs,(InclPoset (Filt (BoolePoset X)))) = Top (InclPoset (Filt (BoolePoset X))) ) ;
hence  "/\" (((f -extension_to_hom) .: Fs),L) = (f -extension_to_hom) . ("/\" (Fs,(InclPoset (Filt (BoolePoset X))))) by Th13; ::_thesis: verum
end;
suppose not Fs is empty ; ::_thesis: "/\" (((f -extension_to_hom) .: Fs),L) = (f -extension_to_hom) . ("/\" (Fs,(InclPoset (Filt (BoolePoset X)))))
then reconsider Fs9 = Fs as non empty Subset of (InclPoset (Filt (BoolePoset X))) ;
defpred S1[ set , set , set ] means X = "/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in L )  }  ,L);
deffunc H1( Element of Fs9) ->  set =  {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in X  }  ;
 not {} in Fs9 ;
then  Fs9 is with_non-empty_elements by SETFAM_1:def_8;
then reconsider K = id Fs9 as V8() ManySortedSet of Fs9 ;
A5: for i being set st i in Fs9 holds
for s being set st s in K . i holds
ex y being set st
( y in (Fs9 --> the carrier of L) . i & S1[y,s,i] )
proof
let i be set ; ::_thesis: ( i in Fs9 implies for s being set st s in K . i holds
ex y being set st
( y in (Fs9 --> the carrier of L) . i & S1[y,s,i] ) )
assume A6: i in Fs9 ; ::_thesis: for s being set st s in K . i holds
ex y being set st
( y in (Fs9 --> the carrier of L) . i & S1[y,s,i] )
let s be set ; ::_thesis: ( s in K . i implies ex y being set st
( y in (Fs9 --> the carrier of L) . i & S1[y,s,i] ) )
assume  s in K . i ; ::_thesis: ex y being set st
( y in (Fs9 --> the carrier of L) . i & S1[y,s,i] )
take y = "/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s )  }  ,L); ::_thesis: ( y in (Fs9 --> the carrier of L) . i & S1[y,s,i] )
 y in the carrier of L ;
hence  y in (Fs9 --> the carrier of L) . i by A6, FUNCOP_1:7; ::_thesis: S1[y,s,i]
thus  S1[y,s,i] ; ::_thesis: verum
end;
consider FD being ManySortedFunction of K,Fs9 --> the carrier of L such that
A7: for i being set st i in Fs9 holds
ex g being Function of (K . i),((Fs9 --> the carrier of L) . i) st
( g = FD . i & ( for s being set st s in K . i holds
S1[g . s,s,i] ) ) from MSSUBFAM:sch_1(A5);
defpred S2[ Element of Fs9] means  rng (FD . X) = H1(X);
A8: for s being Element of Fs9 holds S2[s]
proof
let s be Element of Fs9; ::_thesis: S2[s]
now__::_thesis:_for_t_being_set_holds_
(_(_t_in_rng_(FD_._s)_implies_t_in_H1(s)_)_&_(_t_in_H1(s)_implies_t_in_rng_(FD_._s)_)_)
let t be set ; ::_thesis: ( ( t in rng (FD . s) implies t in H1(s) ) & ( t in H1(s) implies t in rng (FD . s) ) )
consider g being Function of (K . s),((Fs9 --> the carrier of L) . s) such that
A9: g = FD . s and
A10: for u being set st u in K . s holds
S1[g . u,u,s] by A7;
hereby  ::_thesis: ( t in H1(s) implies t in rng (FD . s) )
assume  t in rng (FD . s) ; ::_thesis: t in H1(s)
then consider u being set  such that
A11: u in dom (FD . s) and
A12: t = (FD . s) . u by FUNCT_1:def_3;
consider g being Function of (K . s),((Fs9 --> the carrier of L) . s) such that
A13: g = FD . s and
A14: for u being set st u in K . s holds
S1[g . u,u,s] by A7;
A15: dom (FD . s) = K . s by FUNCT_2:def_1;
A16: g . u = "/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in u )  }  ,L) by A11, A14;
 s in the carrier of (InclPoset (Filt (BoolePoset X))) ;
then  ( K . s = s & ex FF being Filter of (BoolePoset X) st s = FF ) by A1, FUNCT_1:18;
then reconsider u = u as Subset of X by A3, A11, A15, YELLOW_1:4;
 u in s by A11, A15, FUNCT_1:18;
hence  t in H1(s) by A12, A13, A16; ::_thesis: verum
end;
assume  t in H1(s) ; ::_thesis: t in rng (FD . s)
then consider Y being Subset of X such that
A17: t = "/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L) and
A18: Y in s ;
 dom (FD . s) = K . s by FUNCT_2:def_1;
then A19: Y in dom (FD . s) by A18, FUNCT_1:18;
 K . s = s by FUNCT_1:18;
then  g . Y = "/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L) by A18, A10;
hence  t in rng (FD . s) by A17, A19, A9, FUNCT_1:def_3; ::_thesis: verum
end;
hence  S2[s] by TARSKI:1; ::_thesis: verum
end;
 meet Fs9 is Filter of (BoolePoset X) by WAYBEL16:9;
then  meet Fs9 in Filt (BoolePoset X) ;
then reconsider mFs = meet Fs9 as Element of the carrier of (InclPoset (Filt (BoolePoset X))) by A1;
set smFs =  {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in mFs  }  ;
A20: dom FD = Fs9 by PARTFUN1:def_2;
reconsider FD = FD as DoubleIndexedSet of K,L ;
now__::_thesis:_for_r_being_set_holds_
(_(_r_in_(f_-extension_to_hom)_.:_Fs_implies_r_in_rng_(Sups_)_)_&_(_r_in_rng_(Sups_)_implies_r_in_(f_-extension_to_hom)_.:_Fs_)_)
let r be set ; ::_thesis: ( ( r in (f -extension_to_hom) .: Fs implies r in rng (Sups ) ) & ( r in rng (Sups ) implies r in (f -extension_to_hom) .: Fs ) )
hereby  ::_thesis: ( r in rng (Sups ) implies r in (f -extension_to_hom) .: Fs )
assume  r in (f -extension_to_hom) .: Fs ; ::_thesis: r in rng (Sups )
then consider s being set  such that
A21: s in the carrier of (InclPoset (Filt (BoolePoset X))) and
A22: s in Fs and
A23: (f -extension_to_hom) . s = r by FUNCT_2:64;
reconsider s9 = s as Element of the carrier of (InclPoset (Filt (BoolePoset X))) by A21;
reconsider s = s as Element of Fs9 by A22;
A24: S2[s] by A8;
 (f -extension_to_hom) . s9 = "\/" ( {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in s9  }  ,L) by Def3;
then  r = Sup by A23, A24, YELLOW_2:def_5;
hence  r in rng (Sups ) by WAYBEL_5:14; ::_thesis: verum
end;
assume  r in rng (Sups ) ; ::_thesis: r in (f -extension_to_hom) .: Fs
then consider s being Element of Fs9 such that
A25: r = Sup by WAYBEL_5:14;
 S2[s] by A8;
then (f -extension_to_hom) . s = "\/" ((rng (FD . s)),L) by Def3
.= Sup by YELLOW_2:def_5 ;
hence  r in (f -extension_to_hom) .: Fs by A25, FUNCT_2:35; ::_thesis: verum
end;
then  (f -extension_to_hom) .: Fs = rng (Sups ) by TARSKI:1;
then A26: inf ((f -extension_to_hom) .: Fs) = Inf by YELLOW_2:def_6;
A27: now__::_thesis:_for_r_being_set_holds_
(_(_r_in_rng_(Infs_)_implies_r_in__{__("/\"_(_{__(f_._(uparrow_x))_where_x_is_Element_of_(BoolePoset_X)_:_ex_z_being_Element_of_X_st_
(_x_=_{z}_&_z_in_Y_)__}__,L))_where_Y_is_Subset_of_X_:_Y_in_mFs__}__)_&_(_r_in__{__("/\"_(_{__(f_._(uparrow_x))_where_x_is_Element_of_(BoolePoset_X)_:_ex_z_being_Element_of_X_st_
(_x_=_{z}_&_z_in_Y_)__}__,L))_where_Y_is_Subset_of_X_:_Y_in_mFs__}__implies_r_in_rng_(Infs_)_)_)
reconsider pdFD = product (doms FD) as non empty functional set ;
let r be set ; ::_thesis: ( ( r in rng (Infs ) implies r in  {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in mFs  }  ) & ( r in  {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in mFs  }  implies r in rng (Infs ) ) )
reconsider dFFD = (product (doms FD)) --> Fs9 as ManySortedSet of pdFD ;
reconsider FFD = Frege FD as DoubleIndexedSet of dFFD,L ;
deffunc H2( Element of pdFD) ->  set =  {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in X . u )  }  ,L)) where u is Element of Fs9 : u in dom (FFD . X)  }  ;
A28: dom FFD = pdFD by PARTFUN1:def_2;
A29: now__::_thesis:_for_s_being_Element_of_pdFD_holds_rng_(FFD_._s)_=_H2(s)
let s be Element of pdFD; ::_thesis: rng (FFD . s) = H2(s)
A30: dom FD = dom (FFD . s) by A28, WAYBEL_5:8;
now__::_thesis:_for_t_being_set_holds_
(_(_t_in_rng_(FFD_._s)_implies_t_in_H2(s)_)_&_(_t_in_H2(s)_implies_t_in_rng_(FFD_._s)_)_)
let t be set ; ::_thesis: ( ( t in rng (FFD . s) implies t in H2(s) ) & ( t in H2(s) implies t in rng (FFD . s) ) )
hereby  ::_thesis: ( t in H2(s) implies t in rng (FFD . s) )
assume  t in rng (FFD . s) ; ::_thesis: t in H2(s)
then consider u being set  such that
A31: u in dom (FFD . s) and
A32: t = (FFD . s) . u by FUNCT_1:def_3;
A33: (FFD . s) . u = (FD . u) . (s . u) by A28, A30, A31, WAYBEL_5:9;
reconsider u = u as Element of Fs9 by A30, A31;
consider g being Function of (K . u),((Fs9 --> the carrier of L) . u) such that
A34: g = FD . u and
A35: for v being set st v in K . u holds
S1[g . v,v,u] by A7;
 dom (FD . u) = K . u by FUNCT_2:def_1;
then  g . (s . u) = "/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u )  }  ,L) by A20, A28, A35, WAYBEL_5:9;
hence  t in H2(s) by A31, A32, A33, A34; ::_thesis: verum
end;
assume  t in H2(s) ; ::_thesis: t in rng (FFD . s)
then consider u being Element of Fs9 such that
A36: ( t = "/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u )  }  ,L) & u in dom (FFD . s) ) ;
reconsider u = u as Element of Fs9 ;
consider g being Function of (K . u),((Fs9 --> the carrier of L) . u) such that
A37: g = FD . u and
A38: for v being set st v in K . u holds
S1[g . v,v,u] by A7;
 dom (FD . u) = K . u by FUNCT_2:def_1;
then  g . (s . u) = "/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u )  }  ,L) by A20, A28, A38, WAYBEL_5:9;
hence  t in rng (FFD . s) by A28, A30, A36, A37, WAYBEL_5:9; ::_thesis: verum
end;
hence  rng (FFD . s) = H2(s) by TARSKI:1; ::_thesis: verum
end;
hereby  ::_thesis: ( r in  {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in mFs  }  implies r in rng (Infs ) )
assume  r in rng (Infs ) ; ::_thesis: r in  {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in mFs  }
then consider s being Element of pdFD such that
A39: r = Inf by WAYBEL_5:14;
set idFFDs =  {   {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u )  }  where u is Element of Fs9 : u in dom (FFD . s)  }  ;
A40:  {   {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u )  }  where u is Element of Fs9 : u in dom (FFD . s)  }  c= bool the carrier of L
proof
let t be set ; :: according to TARSKI:def_3 ::_thesis: ( not t in  {   {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u )  }  where u is Element of Fs9 : u in dom (FFD . s)  }  or t in bool the carrier of L )
assume  t in  {   {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u )  }  where u is Element of Fs9 : u in dom (FFD . s)  }  ; ::_thesis: t in bool the carrier of L
then consider u being Element of Fs9 such that
A41: t =  {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u )  }  and
 u in dom (FFD . s) ;
 t c= the carrier of L
proof
let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in t or v in the carrier of L )
assume  v in t ; ::_thesis: v in the carrier of L
then consider x being Element of (BoolePoset X) such that
A42: v = f . (uparrow x) and
A43: ex z being Element of X st
( x = {z} & z in s . u ) by A41;
 uparrow x in FixedUltraFilters X by A43;
hence  v in the carrier of L by A42, FUNCT_2:5; ::_thesis: verum
end;
hence  t in bool the carrier of L ; ::_thesis: verum
end;
now__::_thesis:_for_t_being_set_holds_
(_(_t_in_H2(s)_implies_t_in__{__(inf_YY)_where_YY_is_Subset_of_L_:_YY_in__{___{__(f_._(uparrow_x))_where_x_is_Element_of_(BoolePoset_X)_:_ex_z_being_Element_of_X_st_
(_x_=_{z}_&_z_in_s_._u_)__}__where_u_is_Element_of_Fs9_:_u_in_dom_(FFD_._s)__}___}__)_&_(_t_in__{__(inf_YY)_where_YY_is_Subset_of_L_:_YY_in__{___{__(f_._(uparrow_x))_where_x_is_Element_of_(BoolePoset_X)_:_ex_z_being_Element_of_X_st_
(_x_=_{z}_&_z_in_s_._u_)__}__where_u_is_Element_of_Fs9_:_u_in_dom_(FFD_._s)__}___}__implies_t_in_H2(s)_)_)
let t be set ; ::_thesis: ( ( t in H2(s) implies t in  {  (inf YY) where YY is Subset of L : YY in  {   {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u )  }  where u is Element of Fs9 : u in dom (FFD . s)  }   }  ) & ( t in  {  (inf YY) where YY is Subset of L : YY in  {   {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u )  }  where u is Element of Fs9 : u in dom (FFD . s)  }   }  implies t in H2(s) ) )
hereby  ::_thesis: ( t in  {  (inf YY) where YY is Subset of L : YY in  {   {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u )  }  where u is Element of Fs9 : u in dom (FFD . s)  }   }  implies t in H2(s) )
assume  t in H2(s) ; ::_thesis: t in  {  (inf YY) where YY is Subset of L : YY in  {   {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u )  }  where u is Element of Fs9 : u in dom (FFD . s)  }   }
then consider u being Element of Fs9 such that
A44: t = "/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u )  }  ,L) and
A45: u in dom (FFD . s) ;
  {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u )  }  c= the carrier of L
proof
let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in  {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u )  }  or v in the carrier of L )
assume  v in  {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u )  }  ; ::_thesis: v in the carrier of L
then consider x being Element of (BoolePoset X) such that
A46: v = f . (uparrow x) and
A47: ex z being Element of X st
( x = {z} & z in s . u ) ;
 uparrow x in FixedUltraFilters X by A47;
hence  v in the carrier of L by A46, FUNCT_2:5; ::_thesis: verum
end;
then reconsider Y1 =  {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u )  }  as Subset of L ;
 Y1 in  {   {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u )  }  where u is Element of Fs9 : u in dom (FFD . s)  }  by A45;
hence  t in  {  (inf YY) where YY is Subset of L : YY in  {   {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u )  }  where u is Element of Fs9 : u in dom (FFD . s)  }   }  by A44; ::_thesis: verum
end;
assume  t in  {  (inf YY) where YY is Subset of L : YY in  {   {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u )  }  where u is Element of Fs9 : u in dom (FFD . s)  }   }  ; ::_thesis: t in H2(s)
then consider YY being Subset of L such that
A48: t = inf YY and
A49: YY in  {   {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u )  }  where u is Element of Fs9 : u in dom (FFD . s)  }  ;
 ex u1 being Element of Fs9 st
( YY =  {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u1 )  }  & u1 in dom (FFD . s) ) by A49;
hence  t in H2(s) by A48; ::_thesis: verum
end;
then A50: H2(s) =  {  (inf YY) where YY is Subset of L : YY in  {   {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u )  }  where u is Element of Fs9 : u in dom (FFD . s)  }   }  by TARSKI:1;
A51: dom s = dom FD by A28, WAYBEL_5:8;
 union (rng s) c= X
proof
let t be set ; :: according to TARSKI:def_3 ::_thesis: ( not t in union (rng s) or t in X )
assume  t in union (rng s) ; ::_thesis: t in X
then consider te being set  such that
A52: t in te and
A53: te in rng s by TARSKI:def_4;
consider u being set  such that
A54: u in dom s and
A55: te = s . u by A53, FUNCT_1:def_3;
 FD . u is Function of (K . u), the carrier of L by A51, A54, WAYBEL_5:6;
then  dom (FD . u) = K . u by FUNCT_2:def_1
.= u by A51, A54, FUNCT_1:17 ;
then A56: te in u by A28, A51, A54, A55, WAYBEL_5:9;
 u in the carrier of (InclPoset (Filt (BoolePoset X))) by A20, A51, A54;
then  ex FF being Filter of (BoolePoset X) st u = FF by A1;
hence  t in X by A4, A52, A56; ::_thesis: verum
end;
then reconsider Y = union (rng s) as Subset of X ;
set Ys =  {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ;
A57: dom FD = dom (FFD . s) by A28, WAYBEL_5:8;
now__::_thesis:_for_t_being_set_holds_
(_(_t_in_union__{___{__(f_._(uparrow_x))_where_x_is_Element_of_(BoolePoset_X)_:_ex_z_being_Element_of_X_st_
(_x_=_{z}_&_z_in_s_._u_)__}__where_u_is_Element_of_Fs9_:_u_in_dom_(FFD_._s)__}__implies_t_in__{__(f_._(uparrow_x))_where_x_is_Element_of_(BoolePoset_X)_:_ex_z_being_Element_of_X_st_
(_x_=_{z}_&_z_in_Y_)__}__)_&_(_t_in__{__(f_._(uparrow_x))_where_x_is_Element_of_(BoolePoset_X)_:_ex_z_being_Element_of_X_st_
(_x_=_{z}_&_z_in_Y_)__}__implies_t_in_union__{___{__(f_._(uparrow_x))_where_x_is_Element_of_(BoolePoset_X)_:_ex_z_being_Element_of_X_st_
(_x_=_{z}_&_z_in_s_._u_)__}__where_u_is_Element_of_Fs9_:_u_in_dom_(FFD_._s)__}__)_)
let t be set ; ::_thesis: ( ( t in union  {   {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u )  }  where u is Element of Fs9 : u in dom (FFD . s)  }  implies t in  {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ) & ( t in  {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  implies t in union  {   {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u )  }  where u is Element of Fs9 : u in dom (FFD . s)  }  ) )
hereby  ::_thesis: ( t in  {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  implies t in union  {   {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u )  }  where u is Element of Fs9 : u in dom (FFD . s)  }  )
assume  t in union  {   {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u )  }  where u is Element of Fs9 : u in dom (FFD . s)  }  ; ::_thesis: t in  {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }
then consider te being set  such that
A58: t in te and
A59: te in  {   {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u )  }  where u is Element of Fs9 : u in dom (FFD . s)  }  by TARSKI:def_4;
consider u being Element of Fs9 such that
A60: te =  {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u )  }  and
A61: u in dom (FFD . s) by A59;
consider x being Element of (BoolePoset X) such that
A62: t = f . (uparrow x) and
A63: ex z being Element of X st
( x = {z} & z in s . u ) by A58, A60;
consider z being Element of X such that
A64: x = {z} and
A65: z in s . u by A63;
 s . u in rng s by A57, A51, A61, FUNCT_1:def_3;
then  z in Y by A65, TARSKI:def_4;
hence  t in  {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  by A62, A64; ::_thesis: verum
end;
assume  t in  {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ; ::_thesis: t in union  {   {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u )  }  where u is Element of Fs9 : u in dom (FFD . s)  }
then consider x being Element of (BoolePoset X) such that
A66: t = f . (uparrow x) and
A67: ex z being Element of X st
( x = {z} & z in Y ) ;
consider z being Element of X such that
A68: x = {z} and
A69: z in Y by A67;
consider ze being set  such that
A70: z in ze and
A71: ze in rng s by A69, TARSKI:def_4;
consider u being set  such that
A72: u in dom s and
A73: ze = s . u by A71, FUNCT_1:def_3;
reconsider u = u as Element of Fs9 by A51, A72;
A74:  {  (f . (uparrow x1)) where x1 is Element of (BoolePoset X) : ex z being Element of X st
( x1 = {z} & z in s . u )  }  in  {   {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u )  }  where u is Element of Fs9 : u in dom (FFD . s)  }  by A57, A51, A72;
 t in  {  (f . (uparrow x1)) where x1 is Element of (BoolePoset X) : ex z being Element of X st
( x1 = {z} & z in s . u )  }  by A66, A68, A70, A73;
hence  t in union  {   {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u )  }  where u is Element of Fs9 : u in dom (FFD . s)  }  by A74, TARSKI:def_4; ::_thesis: verum
end;
then A75: union  {   {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u )  }  where u is Element of Fs9 : u in dom (FFD . s)  }  =  {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  by TARSKI:1;
now__::_thesis:_for_Z_being_set_st_Z_in_Fs9_holds_
Y_in_Z
reconsider Y9 = Y as Element of (BoolePoset X) by A3, YELLOW_1:4;
let Z be set ; ::_thesis: ( Z in Fs9 implies Y in Z )
assume A76: Z in Fs9 ; ::_thesis: Y in Z
then  FD . Z is Function of (K . Z), the carrier of L by WAYBEL_5:6;
then A77: dom (FD . Z) = K . Z by FUNCT_2:def_1
.= Z by A76, FUNCT_1:17 ;
 s . Z in rng s by A20, A51, A76, FUNCT_1:def_3;
then A78: s . Z c= Y by ZFMISC_1:74;
then reconsider sZ = s . Z as Element of (BoolePoset X) by A2, A3, XBOOLE_1:1;
A79: sZ <= Y9 by A78, YELLOW_1:2;
 Z in the carrier of (InclPoset (Filt (BoolePoset X))) by A76;
then A80: ex FF being Filter of (BoolePoset X) st Z = FF by A1;
 s . Z in dom (FD . Z) by A20, A28, A76, WAYBEL_5:9;
hence  Y in Z by A80, A77, A79, WAYBEL_0:def_20; ::_thesis: verum
end;
then  Y in mFs by SETFAM_1:def_1;
then A81: "/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L) in  {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in mFs  }  ;
"/\" ((rng (FFD . s)),L) = "/\" (H2(s),L) by A29
.= "/\" ((union  {   {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u )  }  where u is Element of Fs9 : u in dom (FFD . s)  }  ),L) by A40, A50, Lm1 ;
hence  r in  {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in mFs  }  by A39, A81, A75, YELLOW_2:def_6; ::_thesis: verum
end;
assume  r in  {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in mFs  }  ; ::_thesis: r in rng (Infs )
then consider Y being Subset of X such that
A82: r = "/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L) and
A83: Y in mFs ;
A84: "/\" ({r},L) = r by A82, YELLOW_0:39;
set s = Fs9 --> Y;
A85: dom (doms FD) = dom FD by FUNCT_6:59
.= dom (Fs9 --> Y) by A20, FUNCOP_1:13 ;
A86: now__::_thesis:_for_w_being_set_st_w_in_dom_(doms_FD)_holds_
(Fs9_-->_Y)_._w_in_(doms_FD)_._w
let w be set ; ::_thesis: ( w in dom (doms FD) implies (Fs9 --> Y) . w in (doms FD) . w )
assume A87: w in dom (doms FD) ; ::_thesis: (Fs9 --> Y) . w in (doms FD) . w
then  FD . w is Function of (K . w),((Fs9 --> the carrier of L) . w) by A85, PBOOLE:def_15;
then A88: dom (FD . w) = K . w by A85, A87, FUNCT_2:def_1
.= w by A85, A87, FUNCT_1:18 ;
 ( (doms FD) . w = dom (FD . w) & (Fs9 --> Y) . w = Y ) by A20, A85, A87, FUNCOP_1:7, FUNCT_6:22;
hence  (Fs9 --> Y) . w in (doms FD) . w by A83, A85, A87, A88, SETFAM_1:def_1; ::_thesis: verum
end;
set s9 = Fs9 --> Y;
reconsider s = Fs9 --> Y as Element of pdFD by A85, A86, CARD_3:9;
now__::_thesis:_for_t_being_set_holds_
(_(_t_in_H2(s)_implies_t_in_{r}_)_&_(_t_in_{r}_implies_t_in_H2(s)_)_)
set u = the Element of Fs9;
let t be set ; ::_thesis: ( ( t in H2(s) implies t in {r} ) & ( t in {r} implies t in H2(s) ) )
A89: ( dom (Fs9 --> Y) = Fs9 & s . the Element of Fs9 = Y ) by FUNCOP_1:7, FUNCOP_1:13;
hereby  ::_thesis: ( t in {r} implies t in H2(s) )
assume  t in H2(s) ; ::_thesis: t in {r}
then consider u being Element of Fs9 such that
A90: t = "/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u )  }  ,L) and
 u in dom (FFD . s) ;
 s . u = Y by FUNCOP_1:7;
hence  t in {r} by A82, A90, TARSKI:def_1; ::_thesis: verum
end;
assume  t in {r} ; ::_thesis: t in H2(s)
then A91: t = r by TARSKI:def_1;
 ( dom FD = dom (FFD . s) & dom s = dom FD ) by A28, WAYBEL_5:8;
hence  t in H2(s) by A82, A91, A89; ::_thesis: verum
end;
then A92:  {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u )  }  ,L)) where u is Element of Fs9 : u in dom (FFD . s)  }  = {r} by TARSKI:1;
 ( Inf = "/\" ((rng (FFD . s)),L) & rng (FFD . s) = H2(s) ) by A29, YELLOW_2:def_6;
hence  r in rng (Infs ) by A92, A84, WAYBEL_5:14; ::_thesis: verum
end;
 for j being Element of Fs9 holds rng (FD . j) is directed
proof
let j be Element of Fs9; ::_thesis: rng (FD . j) is directed
let k, m be Element of L; :: according to WAYBEL_0:def_1 ::_thesis: ( not k in rng (FD . j) or not m in rng (FD . j) or ex b1 being Element of the carrier of L st
( b1 in rng (FD . j) & k <= b1 & m <= b1 ) )
assume that
A93: k in rng (FD . j) and
A94: m in rng (FD . j) ; ::_thesis: ex b1 being Element of the carrier of L st
( b1 in rng (FD . j) & k <= b1 & m <= b1 )
consider kd being set  such that
A95: kd in dom (FD . j) and
A96: (FD . j) . kd = k by A93, FUNCT_1:def_3;
consider md being set  such that
A97: md in dom (FD . j) and
A98: (FD . j) . md = m by A94, FUNCT_1:def_3;
A99: K . j = j by FUNCT_1:18;
 j in the carrier of (InclPoset (Filt (BoolePoset X))) ;
then consider FF being Filter of (BoolePoset X) such that
A100: j = FF by A1;
A101: dom (FD . j) = K . j by FUNCT_2:def_1;
then reconsider kd = kd as Element of (BoolePoset X) by A95, A99, A100;
reconsider md = md as Element of (BoolePoset X) by A97, A101, A99, A100;
consider nd being Element of (BoolePoset X) such that
A102: nd in FF and
A103: nd <= kd and
A104: nd <= md by A95, A97, A99, A100, WAYBEL_0:def_2;
set n = (FD . j) . nd;
A105: (FD . j) . nd in rng (FD . j) by A101, A99, A100, A102, FUNCT_1:def_3;
consider g being Function of (K . j),((Fs9 --> the carrier of L) . j) such that
A106: g = FD . j and
A107: for u being set st u in K . j holds
S1[g . u,u,j] by A7;
set nds =  {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in nd )  }  ;
A108: g . nd = "/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in nd )  }  ,L) by A99, A100, A102, A107;
reconsider n = (FD . j) . nd as Element of L by A105;
take  n ; ::_thesis: ( n in rng (FD . j) & k <= n & m <= n )
thus  n in rng (FD . j) by A101, A99, A100, A102, FUNCT_1:def_3; ::_thesis: ( k <= n & m <= n )
A109: ex_inf_of  {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in nd )  }  ,L by YELLOW_0:17;
set mds =  {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in md )  }  ;
A110: nd c= md by A104, YELLOW_1:2;
A111:  {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in nd )  }  c=  {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in md )  }
proof
let w be set ; :: according to TARSKI:def_3 ::_thesis: ( not w in  {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in nd )  }  or w in  {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in md )  }  )
assume  w in  {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in nd )  }  ; ::_thesis: w in  {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in md )  }
then  ex x being Element of (BoolePoset X) st
( w = f . (uparrow x) & ex z being Element of X st
( x = {z} & z in nd ) ) ;
hence  w in  {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in md )  }  by A110; ::_thesis: verum
end;
A112: ex_inf_of  {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in md )  }  ,L by YELLOW_0:17;
set kds =  {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in kd )  }  ;
A113: ex_inf_of  {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in kd )  }  ,L by YELLOW_0:17;
A114: nd c= kd by A103, YELLOW_1:2;
A115:  {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in nd )  }  c=  {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in kd )  }
proof
let w be set ; :: according to TARSKI:def_3 ::_thesis: ( not w in  {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in nd )  }  or w in  {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in kd )  }  )
assume  w in  {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in nd )  }  ; ::_thesis: w in  {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in kd )  }
then  ex x being Element of (BoolePoset X) st
( w = f . (uparrow x) & ex z being Element of X st
( x = {z} & z in nd ) ) ;
hence  w in  {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in kd )  }  by A114; ::_thesis: verum
end;
 g . kd = "/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in kd )  }  ,L) by A95, A107;
hence  k <= n by A96, A106, A108, A113, A109, A115, YELLOW_0:35; ::_thesis: m <= n
 g . md = "/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in md )  }  ,L) by A97, A107;
hence  m <= n by A98, A106, A108, A109, A112, A111, YELLOW_0:35; ::_thesis: verum
end;
then A116: Inf = Sup by WAYBEL_5:19
.= "\/" ((rng (Infs )),L) by YELLOW_2:def_5 ;
 ( inf Fs9 = meet Fs9 & (f -extension_to_hom) . (meet Fs9) = "\/" ( {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in mFs  }  ,L) ) by Def3, WAYBEL16:10;
hence  "/\" (((f -extension_to_hom) .: Fs),L) = (f -extension_to_hom) . ("/\" (Fs,(InclPoset (Filt (BoolePoset X))))) by A26, A116, A27, TARSKI:1; ::_thesis: verum
end;
end;
end;
end;

theorem Th14: :: WAYBEL22:14
for X being set
for L being non empty complete continuous Poset
for f being Function of (FixedUltraFilters X), the carrier of L holds (f -extension_to_hom) | (FixedUltraFilters X) = f
proof
let X be set ; ::_thesis: for L being non empty complete continuous Poset
for f being Function of (FixedUltraFilters X), the carrier of L holds (f -extension_to_hom) | (FixedUltraFilters X) = f
let L be non empty complete continuous Poset; ::_thesis: for f being Function of (FixedUltraFilters X), the carrier of L holds (f -extension_to_hom) | (FixedUltraFilters X) = f
let f be Function of (FixedUltraFilters X), the carrier of L; ::_thesis: (f -extension_to_hom) | (FixedUltraFilters X) = f
set FUF = FixedUltraFilters X;
set BP = BoolePoset X;
set IP = InclPoset (Filt (BoolePoset X));
A1: InclPoset (Filt (BoolePoset X)) = RelStr(# (Filt (BoolePoset X)),(RelIncl (Filt (BoolePoset X))) #) by YELLOW_1:def_1;
set F = f -extension_to_hom ;
A2: the carrier of (BoolePoset X) = the carrier of (LattPOSet (BooleLatt X)) by YELLOW_1:def_2
.= bool X by LATTICE3:def_1 ;
now__::_thesis:_(_FixedUltraFilters_X_=_dom_((f_-extension_to_hom)_|_(FixedUltraFilters_X))_&_FixedUltraFilters_X_=_dom_f_&_(_for_xf_being_set_st_xf_in_FixedUltraFilters_X_holds_
((f_-extension_to_hom)_|_(FixedUltraFilters_X))_._xf_=_f_._xf_)_)
A3: dom (f -extension_to_hom) = the carrier of (InclPoset (Filt (BoolePoset X))) by FUNCT_2:def_1;
hence  FixedUltraFilters X = dom ((f -extension_to_hom) | (FixedUltraFilters X)) by A1, Th9, RELAT_1:62; ::_thesis: ( FixedUltraFilters X = dom f & ( for xf being set st xf in FixedUltraFilters X holds
((f -extension_to_hom) | (FixedUltraFilters X)) . xf = f . xf ) )
thus  FixedUltraFilters X = dom f by FUNCT_2:def_1; ::_thesis: for xf being set st xf in FixedUltraFilters X holds
((f -extension_to_hom) | (FixedUltraFilters X)) . xf = f . xf
let xf be set ; ::_thesis: ( xf in FixedUltraFilters X implies ((f -extension_to_hom) | (FixedUltraFilters X)) . xf = f . xf )
assume A4: xf in FixedUltraFilters X ; ::_thesis: ((f -extension_to_hom) | (FixedUltraFilters X)) . xf = f . xf
then reconsider FUF9 = FixedUltraFilters X as non empty Subset-Family of (BoolePoset X) ;
A5: ((f -extension_to_hom) | (FixedUltraFilters X)) . xf = (f -extension_to_hom) . xf by A4, FUNCT_1:49;
 FixedUltraFilters X c= dom (f -extension_to_hom) by A1, A3, Th9;
then reconsider x9 = xf as Element of (InclPoset (Filt (BoolePoset X))) by A4, FUNCT_2:def_1;
reconsider xf9 = xf as Element of FUF9 by A4;
set Xs =  {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in x9  }  ;
reconsider f9 = f as Function of FUF9, the carrier of L ;
 f9 . xf9 is Element of L ;
then reconsider fxf = f . xf9 as Element of L ;
consider xx being Element of (BoolePoset X) such that
A6: xf = uparrow xx and
A7: ex y being Element of X st xx = {y} by A4;
A8:  {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in x9  }  is_<=_than fxf
proof
let b be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not b in  {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in x9  }  or b <= fxf )
assume  b in  {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in x9  }  ; ::_thesis: b <= fxf
then consider Y being Subset of X such that
A9: b = "/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L) and
A10: Y in x9 ;
set Xsi =  {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ;
 ex_inf_of  {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L by YELLOW_0:17;
then A11:  {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  is_>=_than b by A9, YELLOW_0:def_10;
reconsider Y = Y as Element of (BoolePoset X) by A6, A10;
consider y being Element of X such that
A12: xx = {y} by A7;
 xx <= Y by A6, A10, WAYBEL_0:18;
then  xx c= Y by YELLOW_1:2;
then  y in Y by A12, ZFMISC_1:31;
then  fxf in  {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  by A6, A12;
hence  b <= fxf by A11, LATTICE3:def_8; ::_thesis: verum
end;
A13: for a being Element of L st  {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in x9  }  is_<=_than a holds
fxf <= a
proof
 xx <= xx ;
then reconsider Y = xx as Element of x9 by A6, WAYBEL_0:18;
set Xsi =  {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ;
consider y being Element of X such that
A14: xx = {y} by A7;
now__::_thesis:_for_p_being_set_holds_
(_(_p_in__{__(f_._(uparrow_x))_where_x_is_Element_of_(BoolePoset_X)_:_ex_z_being_Element_of_X_st_
(_x_=_{z}_&_z_in_Y_)__}__implies_p_in_{fxf}_)_&_(_p_in_{fxf}_implies_p_in__{__(f_._(uparrow_x))_where_x_is_Element_of_(BoolePoset_X)_:_ex_z_being_Element_of_X_st_
(_x_=_{z}_&_z_in_Y_)__}__)_)
let p be set ; ::_thesis: ( ( p in  {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  implies p in {fxf} ) & ( p in {fxf} implies p in  {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ) )
hereby  ::_thesis: ( p in {fxf} implies p in  {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  )
assume  p in  {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ; ::_thesis: p in {fxf}
then consider r being Element of (BoolePoset X) such that
A15: p = f . (uparrow r) and
A16: ex z being Element of X st
( r = {z} & z in Y ) ;
 xx = r by A14, A16, TARSKI:def_1;
hence  p in {fxf} by A6, A15, TARSKI:def_1; ::_thesis: verum
end;
assume  p in {fxf} ; ::_thesis: p in  {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }
then A17: p = fxf by TARSKI:def_1;
 y in Y by A14, TARSKI:def_1;
hence  p in  {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  by A6, A14, A17; ::_thesis: verum
end;
then   {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  = {fxf} by TARSKI:1;
then  fxf = "/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L) by YELLOW_0:39;
then A18: fxf in  {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in x9  }  by A2;
let a be Element of L; ::_thesis: (  {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in x9  }  is_<=_than a implies fxf <= a )
assume   {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in x9  }  is_<=_than a ; ::_thesis: fxf <= a
hence  fxf <= a by A18, LATTICE3:def_9; ::_thesis: verum
end;
 ex_sup_of  {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in x9  }  ,L by YELLOW_0:17;
then  f . xf = "\/" ( {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in x9  }  ,L) by A8, A13, YELLOW_0:def_9;
hence  ((f -extension_to_hom) | (FixedUltraFilters X)) . xf = f . xf by A5, Def3; ::_thesis: verum
end;
hence  (f -extension_to_hom) | (FixedUltraFilters X) = f by FUNCT_1:2; ::_thesis: verum
end;

theorem Th15: :: WAYBEL22:15
for X being set
for L being non empty complete continuous Poset
for f being Function of (FixedUltraFilters X), the carrier of L
for h being CLHomomorphism of InclPoset (Filt (BoolePoset X)),L st h | (FixedUltraFilters X) = f holds
h = f -extension_to_hom
proof
let X be set ; ::_thesis: for L being non empty complete continuous Poset
for f being Function of (FixedUltraFilters X), the carrier of L
for h being CLHomomorphism of InclPoset (Filt (BoolePoset X)),L st h | (FixedUltraFilters X) = f holds
h = f -extension_to_hom
let L be non empty complete continuous Poset; ::_thesis: for f being Function of (FixedUltraFilters X), the carrier of L
for h being CLHomomorphism of InclPoset (Filt (BoolePoset X)),L st h | (FixedUltraFilters X) = f holds
h = f -extension_to_hom
let f be Function of (FixedUltraFilters X), the carrier of L; ::_thesis: for h being CLHomomorphism of InclPoset (Filt (BoolePoset X)),L st h | (FixedUltraFilters X) = f holds
h = f -extension_to_hom
let h be CLHomomorphism of InclPoset (Filt (BoolePoset X)),L; ::_thesis: ( h | (FixedUltraFilters X) = f implies h = f -extension_to_hom )
assume A1: h | (FixedUltraFilters X) = f ; ::_thesis: h = f -extension_to_hom
set F = f -extension_to_hom ;
set cL = the carrier of L;
set BP = BoolePoset X;
set IP = InclPoset (Filt (BoolePoset X));
set cIP = the carrier of (InclPoset (Filt (BoolePoset X)));
A2: InclPoset (Filt (BoolePoset X)) = RelStr(# (Filt (BoolePoset X)),(RelIncl (Filt (BoolePoset X))) #) by YELLOW_1:def_1;
reconsider F9 = f -extension_to_hom as Function of the carrier of (InclPoset (Filt (BoolePoset X))), the carrier of L ;
reconsider h9 = h as Function of the carrier of (InclPoset (Filt (BoolePoset X))), the carrier of L ;
A3: the carrier of (BoolePoset X) = the carrier of (LattPOSet (BooleLatt X)) by YELLOW_1:def_2
.= bool X by LATTICE3:def_1 ;
now__::_thesis:_for_Fi_being_Element_of_the_carrier_of_(InclPoset_(Filt_(BoolePoset_X)))_holds_h9_._Fi_=_F9_._Fi
set FUF = FixedUltraFilters X;
let Fi be Element of the carrier of (InclPoset (Filt (BoolePoset X))); ::_thesis: h9 . Fi = F9 . Fi
 Fi in Filt (BoolePoset X) by A2;
then consider FF being Filter of (BoolePoset X) such that
A4: Fi = FF ;
set Xsf =  {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in FF  }  ;
set Xs =  {  ("/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in FF  }  ;
A5:  {  ("/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in FF  }  c= the carrier of (InclPoset (Filt (BoolePoset X)))
proof
let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in  {  ("/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in FF  }  or p in the carrier of (InclPoset (Filt (BoolePoset X))) )
assume  p in  {  ("/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in FF  }  ; ::_thesis: p in the carrier of (InclPoset (Filt (BoolePoset X)))
then  ex YY being Subset of X st
( p = "/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in YY )  }  ,(InclPoset (Filt (BoolePoset X)))) & YY in FF ) ;
hence  p in the carrier of (InclPoset (Filt (BoolePoset X))) ; ::_thesis: verum
end;
now__::_thesis:_not__{__("/\"_(_{__(uparrow_x)_where_x_is_Element_of_(BoolePoset_X)_:_ex_z_being_Element_of_X_st_
(_x_=_{z}_&_z_in_Y_)__}__,(InclPoset_(Filt_(BoolePoset_X)))))_where_Y_is_Subset_of_X_:_Y_in_FF__}__is_empty
consider YY being set  such that
A6: YY in FF by XBOOLE_0:def_1;
 "/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in YY )  }  ,(InclPoset (Filt (BoolePoset X)))) in  {  ("/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in FF  }  by A3, A6;
hence  not  {  ("/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in FF  }  is empty ; ::_thesis: verum
end;
then reconsider Xs =  {  ("/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in FF  }  as non empty Subset of (InclPoset (Filt (BoolePoset X))) by A5;
A7: ex_sup_of Xs, InclPoset (Filt (BoolePoset X)) by YELLOW_0:17;
A8: Xs is directed
proof
let a, b be Element of (InclPoset (Filt (BoolePoset X))); :: according to WAYBEL_0:def_1 ::_thesis: ( not a in Xs or not b in Xs or ex b1 being Element of the carrier of (InclPoset (Filt (BoolePoset X))) st
( b1 in Xs & a <= b1 & b <= b1 ) )
assume that
A9: a in Xs and
A10: b in Xs ; ::_thesis: ex b1 being Element of the carrier of (InclPoset (Filt (BoolePoset X))) st
( b1 in Xs & a <= b1 & b <= b1 )
consider Yb being Subset of X such that
A11: b = "/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yb )  }  ,(InclPoset (Filt (BoolePoset X)))) and
A12: Yb in FF by A10;
reconsider Yb9 = Yb as Element of FF by A12;
set Xsb =  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yb )  }  ;
consider Ya being Subset of X such that
A13: a = "/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Ya )  }  ,(InclPoset (Filt (BoolePoset X)))) and
A14: Ya in FF by A9;
reconsider Ya9 = Ya as Element of FF by A14;
set Xsa =  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Ya )  }  ;
percases (  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Ya )  }  is empty or  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yb )  }  is empty or ( not  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Ya )  }  is empty & not  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yb )  }  is empty ) ) ;
supposeA15:  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Ya )  }  is empty ; ::_thesis: ex b1 being Element of the carrier of (InclPoset (Filt (BoolePoset X))) st
( b1 in Xs & a <= b1 & b <= b1 )
take  a ; ::_thesis: ( a in Xs & a <= a & b <= a )
thus  a in Xs by A9; ::_thesis: ( a <= a & b <= a )
thus  a <= a ; ::_thesis: b <= a
 "/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Ya )  }  ,(InclPoset (Filt (BoolePoset X)))) = Top (InclPoset (Filt (BoolePoset X))) by A15;
hence  b <= a by A13, YELLOW_0:45; ::_thesis: verum
end;
supposeA16:  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yb )  }  is empty ; ::_thesis: ex b1 being Element of the carrier of (InclPoset (Filt (BoolePoset X))) st
( b1 in Xs & a <= b1 & b <= b1 )
take  b ; ::_thesis: ( b in Xs & a <= b & b <= b )
thus  b in Xs by A10; ::_thesis: ( a <= b & b <= b )
 "/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yb )  }  ,(InclPoset (Filt (BoolePoset X)))) = Top (InclPoset (Filt (BoolePoset X))) by A16;
hence  a <= b by A11, YELLOW_0:45; ::_thesis: b <= b
thus  b <= b ; ::_thesis: verum
end;
supposeA17: ( not  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Ya )  }  is empty & not  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yb )  }  is empty ) ; ::_thesis: ex b1 being Element of the carrier of (InclPoset (Filt (BoolePoset X))) st
( b1 in Xs & a <= b1 & b <= b1 )
  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yb )  }  c= the carrier of (InclPoset (Filt (BoolePoset X)))
proof
let r be set ; :: according to TARSKI:def_3 ::_thesis: ( not r in  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yb )  }  or r in the carrier of (InclPoset (Filt (BoolePoset X))) )
assume  r in  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yb )  }  ; ::_thesis: r in the carrier of (InclPoset (Filt (BoolePoset X)))
then  ex xz being Element of (BoolePoset X) st
( r = uparrow xz & ex z being Element of X st
( xz = {z} & z in Yb ) ) ;
hence  r in the carrier of (InclPoset (Filt (BoolePoset X))) by A2; ::_thesis: verum
end;
then reconsider Xsb =  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yb )  }  as non empty Subset of (InclPoset (Filt (BoolePoset X))) by A17;
  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Ya )  }  c= the carrier of (InclPoset (Filt (BoolePoset X)))
proof
let r be set ; :: according to TARSKI:def_3 ::_thesis: ( not r in  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Ya )  }  or r in the carrier of (InclPoset (Filt (BoolePoset X))) )
assume  r in  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Ya )  }  ; ::_thesis: r in the carrier of (InclPoset (Filt (BoolePoset X)))
then  ex xz being Element of (BoolePoset X) st
( r = uparrow xz & ex z being Element of X st
( xz = {z} & z in Ya ) ) ;
hence  r in the carrier of (InclPoset (Filt (BoolePoset X))) by A2; ::_thesis: verum
end;
then reconsider Xsa =  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Ya )  }  as non empty Subset of (InclPoset (Filt (BoolePoset X))) by A17;
A18: "/\" (Xsb,(InclPoset (Filt (BoolePoset X)))) = meet Xsb by WAYBEL16:10;
consider Yab being Element of (BoolePoset X) such that
A19: Yab in FF and
A20: Yab <= Ya9 and
A21: Yab <= Yb9 by WAYBEL_0:def_2;
reconsider Yab = Yab as Element of FF by A19;
set c = "/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab )  }  ,(InclPoset (Filt (BoolePoset X))));
set Xsc =  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab )  }  ;
A22: "/\" (Xsa,(InclPoset (Filt (BoolePoset X)))) = meet Xsa by WAYBEL16:10;
thus  ex b1 being Element of the carrier of (InclPoset (Filt (BoolePoset X))) st
( b1 in Xs & a <= b1 & b <= b1 ) ::_thesis: verum
proof
percases (  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab )  }  is empty or not  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab )  }  is empty ) ;
supposeA23:  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab )  }  is empty ; ::_thesis: ex b1 being Element of the carrier of (InclPoset (Filt (BoolePoset X))) st
( b1 in Xs & a <= b1 & b <= b1 )
take  "/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab )  }  ,(InclPoset (Filt (BoolePoset X)))) ; ::_thesis: ( "/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab )  }  ,(InclPoset (Filt (BoolePoset X)))) in Xs & a <= "/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab )  }  ,(InclPoset (Filt (BoolePoset X)))) & b <= "/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab )  }  ,(InclPoset (Filt (BoolePoset X)))) )
thus  "/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab )  }  ,(InclPoset (Filt (BoolePoset X)))) in Xs by A3; ::_thesis: ( a <= "/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab )  }  ,(InclPoset (Filt (BoolePoset X)))) & b <= "/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab )  }  ,(InclPoset (Filt (BoolePoset X)))) )
A24: "/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab )  }  ,(InclPoset (Filt (BoolePoset X)))) = Top (InclPoset (Filt (BoolePoset X))) by A23;
hence  a <= "/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab )  }  ,(InclPoset (Filt (BoolePoset X)))) by YELLOW_0:45; ::_thesis: b <= "/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab )  }  ,(InclPoset (Filt (BoolePoset X))))
thus  b <= "/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab )  }  ,(InclPoset (Filt (BoolePoset X)))) by A24, YELLOW_0:45; ::_thesis: verum
end;
supposeA25: not  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab )  }  is empty ; ::_thesis: ex b1 being Element of the carrier of (InclPoset (Filt (BoolePoset X))) st
( b1 in Xs & a <= b1 & b <= b1 )
  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab )  }  c= the carrier of (InclPoset (Filt (BoolePoset X)))
proof
let r be set ; :: according to TARSKI:def_3 ::_thesis: ( not r in  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab )  }  or r in the carrier of (InclPoset (Filt (BoolePoset X))) )
assume  r in  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab )  }  ; ::_thesis: r in the carrier of (InclPoset (Filt (BoolePoset X)))
then  ex xz being Element of (BoolePoset X) st
( r = uparrow xz & ex z being Element of X st
( xz = {z} & z in Yab ) ) ;
hence  r in the carrier of (InclPoset (Filt (BoolePoset X))) by A2; ::_thesis: verum
end;
then reconsider Xsc =  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab )  }  as non empty Subset of (InclPoset (Filt (BoolePoset X))) by A25;
take  "/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab )  }  ,(InclPoset (Filt (BoolePoset X)))) ; ::_thesis: ( "/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab )  }  ,(InclPoset (Filt (BoolePoset X)))) in Xs & a <= "/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab )  }  ,(InclPoset (Filt (BoolePoset X)))) & b <= "/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab )  }  ,(InclPoset (Filt (BoolePoset X)))) )
thus  "/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab )  }  ,(InclPoset (Filt (BoolePoset X)))) in Xs by A3; ::_thesis: ( a <= "/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab )  }  ,(InclPoset (Filt (BoolePoset X)))) & b <= "/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab )  }  ,(InclPoset (Filt (BoolePoset X)))) )
A26: "/\" (Xsc,(InclPoset (Filt (BoolePoset X)))) = meet Xsc by WAYBEL16:10;
 a c= "/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab )  }  ,(InclPoset (Filt (BoolePoset X))))
proof
let d be set ; :: according to TARSKI:def_3 ::_thesis: ( not d in a or d in "/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab )  }  ,(InclPoset (Filt (BoolePoset X)))) )
 Xsc c= Xsa
proof
let r be set ; :: according to TARSKI:def_3 ::_thesis: ( not r in Xsc or r in Xsa )
assume  r in Xsc ; ::_thesis: r in Xsa
then A27: ex xz being Element of (BoolePoset X) st
( r = uparrow xz & ex z being Element of X st
( xz = {z} & z in Yab ) ) ;
 Yab c= Ya by A20, YELLOW_1:2;
hence  r in Xsa by A27; ::_thesis: verum
end;
then A28: meet Xsa c= meet Xsc by SETFAM_1:6;
assume  d in a ; ::_thesis: d in "/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab )  }  ,(InclPoset (Filt (BoolePoset X))))
hence  d in "/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab )  }  ,(InclPoset (Filt (BoolePoset X)))) by A13, A22, A26, A28; ::_thesis: verum
end;
hence  a <= "/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab )  }  ,(InclPoset (Filt (BoolePoset X)))) by YELLOW_1:3; ::_thesis: b <= "/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab )  }  ,(InclPoset (Filt (BoolePoset X))))
 b c= "/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab )  }  ,(InclPoset (Filt (BoolePoset X))))
proof
let d be set ; :: according to TARSKI:def_3 ::_thesis: ( not d in b or d in "/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab )  }  ,(InclPoset (Filt (BoolePoset X)))) )
 Xsc c= Xsb
proof
let r be set ; :: according to TARSKI:def_3 ::_thesis: ( not r in Xsc or r in Xsb )
assume  r in Xsc ; ::_thesis: r in Xsb
then A29: ex xz being Element of (BoolePoset X) st
( r = uparrow xz & ex z being Element of X st
( xz = {z} & z in Yab ) ) ;
 Yab c= Yb by A21, YELLOW_1:2;
hence  r in Xsb by A29; ::_thesis: verum
end;
then A30: meet Xsb c= meet Xsc by SETFAM_1:6;
assume  d in b ; ::_thesis: d in "/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab )  }  ,(InclPoset (Filt (BoolePoset X))))
hence  d in "/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab )  }  ,(InclPoset (Filt (BoolePoset X)))) by A11, A18, A26, A30; ::_thesis: verum
end;
hence  b <= "/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab )  }  ,(InclPoset (Filt (BoolePoset X)))) by YELLOW_1:3; ::_thesis: verum
end;
end;
end;
end;
end;
end;
A31: h is infs-preserving by WAYBEL16:def_1;
now__::_thesis:_for_s_being_set_holds_
(_(_s_in_h_.:_Xs_implies_s_in__{__("/\"_(_{__(f_._(uparrow_x))_where_x_is_Element_of_(BoolePoset_X)_:_ex_z_being_Element_of_X_st_
(_x_=_{z}_&_z_in_Y_)__}__,L))_where_Y_is_Subset_of_X_:_Y_in_FF__}__)_&_(_s_in__{__("/\"_(_{__(f_._(uparrow_x))_where_x_is_Element_of_(BoolePoset_X)_:_ex_z_being_Element_of_X_st_
(_x_=_{z}_&_z_in_Y_)__}__,L))_where_Y_is_Subset_of_X_:_Y_in_FF__}__implies_s_in_h_.:_Xs_)_)
let s be set ; ::_thesis: ( ( s in h .: Xs implies s in  {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in FF  }  ) & ( s in  {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in FF  }  implies s in h .: Xs ) )
hereby  ::_thesis: ( s in  {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in FF  }  implies s in h .: Xs )
assume  s in h .: Xs ; ::_thesis: s in  {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in FF  }
then consider t being set  such that
 t in the carrier of (InclPoset (Filt (BoolePoset X))) and
A32: t in Xs and
A33: s = h . t by FUNCT_2:64;
consider Y being Subset of X such that
A34: ( t = "/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,(InclPoset (Filt (BoolePoset X)))) & Y in FF ) by A32;
set Xsi =  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ;
  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  c= the carrier of (InclPoset (Filt (BoolePoset X)))
proof
let r be set ; :: according to TARSKI:def_3 ::_thesis: ( not r in  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  or r in the carrier of (InclPoset (Filt (BoolePoset X))) )
assume  r in  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ; ::_thesis: r in the carrier of (InclPoset (Filt (BoolePoset X)))
then  ex xz being Element of (BoolePoset X) st
( r = uparrow xz & ex z being Element of X st
( xz = {z} & z in Y ) ) ;
hence  r in the carrier of (InclPoset (Filt (BoolePoset X))) by A2; ::_thesis: verum
end;
then reconsider Xsi =  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  as Subset of (InclPoset (Filt (BoolePoset X))) ;
set Xsif =  {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ;
now__::_thesis:_for_u_being_set_holds_
(_(_u_in_h_.:_Xsi_implies_u_in__{__(f_._(uparrow_x))_where_x_is_Element_of_(BoolePoset_X)_:_ex_z_being_Element_of_X_st_
(_x_=_{z}_&_z_in_Y_)__}__)_&_(_u_in__{__(f_._(uparrow_x))_where_x_is_Element_of_(BoolePoset_X)_:_ex_z_being_Element_of_X_st_
(_x_=_{z}_&_z_in_Y_)__}__implies_u_in_h_.:_Xsi_)_)
let u be set ; ::_thesis: ( ( u in h .: Xsi implies u in  {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ) & ( u in  {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  implies u in h .: Xsi ) )
hereby  ::_thesis: ( u in  {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  implies u in h .: Xsi )
assume  u in h .: Xsi ; ::_thesis: u in  {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }
then consider v being set  such that
 v in the carrier of (InclPoset (Filt (BoolePoset X))) and
A35: v in Xsi and
A36: u = h . v by FUNCT_2:64;
A37: ex x being Element of (BoolePoset X) st
( v = uparrow x & ex z being Element of X st
( x = {z} & z in Y ) ) by A35;
then  v in FixedUltraFilters X ;
then  h . v = f . v by A1, FUNCT_1:49;
hence  u in  {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  by A36, A37; ::_thesis: verum
end;
assume  u in  {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ; ::_thesis: u in h .: Xsi
then consider x being Element of (BoolePoset X) such that
A38: u = f . (uparrow x) and
A39: ex z being Element of X st
( x = {z} & z in Y ) ;
 uparrow x in FixedUltraFilters X by A39;
then A40: h . (uparrow x) = f . (uparrow x) by A1, FUNCT_1:49;
 uparrow x in Xsi by A39;
hence  u in h .: Xsi by A38, A40, FUNCT_2:35; ::_thesis: verum
end;
then A41: h .: Xsi =  {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  by TARSKI:1;
 ( h preserves_inf_of Xsi & ex_inf_of Xsi, InclPoset (Filt (BoolePoset X)) ) by A31, WAYBEL_0:def_32, YELLOW_0:17;
then  inf (h .: Xsi) = h . (inf Xsi) by WAYBEL_0:def_30;
hence  s in  {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in FF  }  by A33, A34, A41; ::_thesis: verum
end;
assume  s in  {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in FF  }  ; ::_thesis: s in h .: Xs
then consider Y being Subset of X such that
A42: s = "/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L) and
A43: Y in FF ;
set Xsi =  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ;
  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  c= the carrier of (InclPoset (Filt (BoolePoset X)))
proof
let r be set ; :: according to TARSKI:def_3 ::_thesis: ( not r in  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  or r in the carrier of (InclPoset (Filt (BoolePoset X))) )
assume  r in  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ; ::_thesis: r in the carrier of (InclPoset (Filt (BoolePoset X)))
then  ex xz being Element of (BoolePoset X) st
( r = uparrow xz & ex z being Element of X st
( xz = {z} & z in Y ) ) ;
hence  r in the carrier of (InclPoset (Filt (BoolePoset X))) by A2; ::_thesis: verum
end;
then reconsider Xsi =  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  as Subset of (InclPoset (Filt (BoolePoset X))) ;
set Xsif =  {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ;
 ( h preserves_inf_of Xsi & ex_inf_of Xsi, InclPoset (Filt (BoolePoset X)) ) by A31, WAYBEL_0:def_32, YELLOW_0:17;
then A44: inf (h .: Xsi) = h . (inf Xsi) by WAYBEL_0:def_30;
now__::_thesis:_for_u_being_set_holds_
(_(_u_in_h_.:_Xsi_implies_u_in__{__(f_._(uparrow_x))_where_x_is_Element_of_(BoolePoset_X)_:_ex_z_being_Element_of_X_st_
(_x_=_{z}_&_z_in_Y_)__}__)_&_(_u_in__{__(f_._(uparrow_x))_where_x_is_Element_of_(BoolePoset_X)_:_ex_z_being_Element_of_X_st_
(_x_=_{z}_&_z_in_Y_)__}__implies_u_in_h_.:_Xsi_)_)
let u be set ; ::_thesis: ( ( u in h .: Xsi implies u in  {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ) & ( u in  {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  implies u in h .: Xsi ) )
hereby  ::_thesis: ( u in  {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  implies u in h .: Xsi )
assume  u in h .: Xsi ; ::_thesis: u in  {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }
then consider v being set  such that
 v in the carrier of (InclPoset (Filt (BoolePoset X))) and
A45: v in Xsi and
A46: u = h . v by FUNCT_2:64;
A47: ex x being Element of (BoolePoset X) st
( v = uparrow x & ex z being Element of X st
( x = {z} & z in Y ) ) by A45;
then  v in FixedUltraFilters X ;
then  h . v = f . v by A1, FUNCT_1:49;
hence  u in  {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  by A46, A47; ::_thesis: verum
end;
assume  u in  {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ; ::_thesis: u in h .: Xsi
then consider x being Element of (BoolePoset X) such that
A48: u = f . (uparrow x) and
A49: ex z being Element of X st
( x = {z} & z in Y ) ;
 uparrow x in FixedUltraFilters X by A49;
then A50: h . (uparrow x) = f . (uparrow x) by A1, FUNCT_1:49;
 uparrow x in Xsi by A49;
hence  u in h .: Xsi by A48, A50, FUNCT_2:35; ::_thesis: verum
end;
then A51: h .: Xsi =  {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  by TARSKI:1;
 inf Xsi in Xs by A43;
hence  s in h .: Xs by A42, A44, A51, FUNCT_2:35; ::_thesis: verum
end;
then A52: h .: Xs =  {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in FF  }  by TARSKI:1;
A53: FF = "\/" ( {  ("/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in FF  }  ,(InclPoset (Filt (BoolePoset X)))) by Th11;
 h is directed-sups-preserving by WAYBEL16:def_1;
then  h preserves_sup_of Xs by A8, WAYBEL_0:def_37;
hence h9 . Fi = sup (h .: Xs) by A4, A53, A7, WAYBEL_0:def_31
.= F9 . Fi by A4, A52, Def3 ;
::_thesis: verum
end;
hence  h = f -extension_to_hom by FUNCT_2:63; ::_thesis: verum
end;

theorem Th16: :: WAYBEL22:16
for X being set holds FixedUltraFilters X is_FreeGen_set_of InclPoset (Filt (BoolePoset X))
proof
let X be set ; ::_thesis: FixedUltraFilters X is_FreeGen_set_of InclPoset (Filt (BoolePoset X))
set FUF = FixedUltraFilters X;
set IP = InclPoset (Filt (BoolePoset X));
let L be non empty complete continuous Poset; :: according to WAYBEL22:def_1 ::_thesis: for f being Function of (FixedUltraFilters X), the carrier of L ex h being CLHomomorphism of InclPoset (Filt (BoolePoset X)),L st
( h | (FixedUltraFilters X) = f & ( for h9 being CLHomomorphism of InclPoset (Filt (BoolePoset X)),L st h9 | (FixedUltraFilters X) = f holds
h9 = h ) )
let f be Function of (FixedUltraFilters X), the carrier of L; ::_thesis: ex h being CLHomomorphism of InclPoset (Filt (BoolePoset X)),L st
( h | (FixedUltraFilters X) = f & ( for h9 being CLHomomorphism of InclPoset (Filt (BoolePoset X)),L st h9 | (FixedUltraFilters X) = f holds
h9 = h ) )
reconsider F = f -extension_to_hom as CLHomomorphism of InclPoset (Filt (BoolePoset X)),L by WAYBEL16:def_1;
take  F ; ::_thesis: ( F | (FixedUltraFilters X) = f & ( for h9 being CLHomomorphism of InclPoset (Filt (BoolePoset X)),L st h9 | (FixedUltraFilters X) = f holds
h9 = F ) )
thus  F | (FixedUltraFilters X) = f by Th14; ::_thesis: for h9 being CLHomomorphism of InclPoset (Filt (BoolePoset X)),L st h9 | (FixedUltraFilters X) = f holds
h9 = F
let h9 be CLHomomorphism of InclPoset (Filt (BoolePoset X)),L; ::_thesis: ( h9 | (FixedUltraFilters X) = f implies h9 = F )
assume  h9 | (FixedUltraFilters X) = f ; ::_thesis: h9 = F
hence  h9 = F by Th15; ::_thesis: verum
end;

theorem Th17: :: WAYBEL22:17
for L, M being complete continuous LATTICE
for F, G being set st F is_FreeGen_set_of L & G is_FreeGen_set_of M & card F = card G holds
L,M are_isomorphic
proof
let L, M be complete continuous LATTICE; ::_thesis: for F, G being set st F is_FreeGen_set_of L & G is_FreeGen_set_of M & card F = card G holds
L,M are_isomorphic
let Lg, Mg be set ; ::_thesis: ( Lg is_FreeGen_set_of L & Mg is_FreeGen_set_of M & card Lg = card Mg implies L,M are_isomorphic )
assume that
A1: Lg is_FreeGen_set_of L and
A2: Mg is_FreeGen_set_of M and
A3: card Lg = card Mg ; ::_thesis: L,M are_isomorphic
 Lg,Mg are_equipotent by A3, CARD_1:5;
then consider f being Function such that
A4: f is one-to-one and
A5: dom f = Lg and
A6: rng f = Mg by WELLORD2:def_4;
set g = f " ;
A7: dom (f ") = Mg by A4, A6, FUNCT_1:33;
reconsider Mg = Mg as Subset of M by A2, Th7;
A8: rng (f ") = Lg by A4, A5, FUNCT_1:33;
reconsider Lg = Lg as Subset of L by A1, Th7;
 Mg c= the carrier of M ;
then reconsider f = f as Function of Lg, the carrier of M by A5, A6, FUNCT_2:def_1, RELSET_1:4;
consider F being CLHomomorphism of L,M such that
A9: F | Lg = f and
 for h9 being CLHomomorphism of L,M st h9 | Lg = f holds
h9 = F by A1, Def1;
 Lg c= the carrier of L ;
then reconsider g = f " as Function of Mg, the carrier of L by A7, A8, FUNCT_2:def_1, RELSET_1:4;
consider G being CLHomomorphism of M,L such that
A10: G | Mg = g and
 for h9 being CLHomomorphism of M,L st h9 | Mg = g holds
h9 = G by A2, Def1;
reconsider GF = G * F as CLHomomorphism of L,L by Th2;
GF | Lg = G * f by A9, RELAT_1:83
.= g * f by A6, A10, FUNCT_4:2
.= id Lg by A4, A5, FUNCT_1:39 ;
then A11: GF = id L by A1, Th8;
then A12: F is V13() by FUNCT_2:23;
reconsider FG = F * G as CLHomomorphism of M,M by Th2;
 F is directed-sups-preserving by WAYBEL16:def_1;
then A13: F is monotone by WAYBEL17:3;
 G is directed-sups-preserving by WAYBEL16:def_1;
then A14: G is monotone by WAYBEL17:3;
FG | Mg = F * g by A10, RELAT_1:83
.= f * g by A8, A9, FUNCT_4:2
.= id Mg by A4, A6, FUNCT_1:39 ;
then  FG = id M by A2, Th8;
then  F is onto by FUNCT_2:23;
then  rng F = the carrier of M by FUNCT_2:def_3;
then  G = F " by A11, A12, FUNCT_2:30;
then  F is isomorphic by A12, A13, A14, WAYBEL_0:def_38;
hence  L,M are_isomorphic by WAYBEL_1:def_8; ::_thesis: verum
end;

theorem :: WAYBEL22:18
for X being set
for L being complete continuous LATTICE
for G being set st G is_FreeGen_set_of L & card G = card X holds
L, InclPoset (Filt (BoolePoset X)) are_isomorphic
proof
let X be set ; ::_thesis: for L being complete continuous LATTICE
for G being set st G is_FreeGen_set_of L & card G = card X holds
L, InclPoset (Filt (BoolePoset X)) are_isomorphic
A1: ( FixedUltraFilters X is_FreeGen_set_of InclPoset (Filt (BoolePoset X)) & card X = card (FixedUltraFilters X) ) by Th10, Th16;
let L be complete continuous LATTICE; ::_thesis: for G being set st G is_FreeGen_set_of L & card G = card X holds
L, InclPoset (Filt (BoolePoset X)) are_isomorphic
let G be set ; ::_thesis: ( G is_FreeGen_set_of L & card G = card X implies L, InclPoset (Filt (BoolePoset X)) are_isomorphic )
assume  ( G is_FreeGen_set_of L & card G = card X ) ; ::_thesis: L, InclPoset (Filt (BoolePoset X)) are_isomorphic
hence  L, InclPoset (Filt (BoolePoset X)) are_isomorphic by A1, Th17; ::_thesis: verum
end;