:: WAYBEL12 semantic presentation

begin

Lm1:  for L being non empty RelStr
for f being Function of NAT, the carrier of L
for n being Element of NAT holds  {  (f . k) where k is Element of NAT : k <= n  }  is non empty finite Subset of L
proof
let L be non empty RelStr ; ::_thesis: for f being Function of NAT, the carrier of L
for n being Element of NAT holds  {  (f . k) where k is Element of NAT : k <= n  }  is non empty finite Subset of L
let f be Function of NAT, the carrier of L; ::_thesis: for n being Element of NAT holds  {  (f . k) where k is Element of NAT : k <= n  }  is non empty finite Subset of L
let n be Element of NAT ; ::_thesis:  {  (f . k) where k is Element of NAT : k <= n  }  is non empty finite Subset of L
set A =  {  (f . m) where m is Element of NAT : m <= n  }  ;
A1:  {  (f . m) where m is Element of NAT : m <= n  }  c=  {  (f . m) where m is Element of NAT : m in {0} \/ (Seg n)  }
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in  {  (f . m) where m is Element of NAT : m <= n  }  or q in  {  (f . m) where m is Element of NAT : m in {0} \/ (Seg n)  }  )
assume  q in  {  (f . m) where m is Element of NAT : m <= n  }  ; ::_thesis: q in  {  (f . m) where m is Element of NAT : m in {0} \/ (Seg n)  }
then consider m being Element of NAT  such that
A2: q = f . m and
A3: m <= n ;
A4: ( m = 0 or m in Seg m ) by FINSEQ_1:3;
 Seg m c= Seg n by A3, FINSEQ_1:5;
then  ( m in {0} or m in Seg n ) by A4, TARSKI:def_1;
then  m in {0} \/ (Seg n) by XBOOLE_0:def_3;
hence  q in  {  (f . m) where m is Element of NAT : m in {0} \/ (Seg n)  }  by A2; ::_thesis: verum
end;
deffunc H1( set ) ->  set = f . $1;
A5:  {  (f . m) where m is Element of NAT : m <= n  }  c= the carrier of L
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in  {  (f . m) where m is Element of NAT : m <= n  }  or q in the carrier of L )
assume  q in  {  (f . m) where m is Element of NAT : m <= n  }  ; ::_thesis: q in the carrier of L
then  ex m being Element of NAT st
( q = f . m & m <= n ) ;
hence  q in the carrier of L ; ::_thesis: verum
end;
 card  {  H1(m) where m is Element of NAT : m in {0} \/ (Seg n)  }  c= card ({0} \/ (Seg n)) from TREES_2:sch_2();
then A6:  {  (f . m) where m is Element of NAT : m in {0} \/ (Seg n)  }  is finite ;
 0 <= n by NAT_1:2;
then  f . 0 in  {  (f . m) where m is Element of NAT : m <= n  }  ;
hence   {  (f . k) where k is Element of NAT : k <= n  }  is non empty finite Subset of L by A1, A6, A5; ::_thesis: verum
end;

definition
let T be TopStruct ;
let P be Subset of T;
redefine attr P is closed  means :: WAYBEL12:def 1
P ` is open ;
compatibility
 ( P is closed iff P ` is open )
proof
hereby  ::_thesis: ( P ` is open implies P is closed )
assume  P is closed ; ::_thesis: P ` is open
then  ([#] T) \ P is open by PRE_TOPC:def_3;
hence  P ` is open ; ::_thesis: verum
end;
assume  P ` is open ; ::_thesis: P is closed
hence  ([#] T) \ P is open ; :: according to PRE_TOPC:def_3 ::_thesis: verum
end;
end;

:: deftheorem  defines closed WAYBEL12:def_1_:_
 for T being TopStruct
for P being Subset of T holds
( P is closed iff P ` is open );

definition
let T be TopStruct ;
let F be Subset-Family of T;
attrF is dense  means :Def2: :: WAYBEL12:def 2
 for X being Subset of T st X in F holds
X is dense ;
end;

:: deftheorem Def2 defines dense WAYBEL12:def_2_:_
 for T being TopStruct
for F being Subset-Family of T holds
( F is dense iff for X being Subset of T st X in F holds
X is dense );

theorem Th1: :: WAYBEL12:1
for X, Y being set st card X c= card Y & Y is countable holds
X is countable
proof
let X, Y be set ; ::_thesis: ( card X c= card Y & Y is countable implies X is countable )
assume A1: card X c= card Y ; ::_thesis: ( not Y is countable or X is countable )
assume  card Y c= omega ; :: according to CARD_3:def_14 ::_thesis: X is countable
hence  card X c= omega by A1, XBOOLE_1:1; :: according to CARD_3:def_14 ::_thesis: verum
end;

theorem :: WAYBEL12:2
for A being denumerable set holds NAT ,A are_equipotent
proof
let A be denumerable set ; ::_thesis: NAT ,A are_equipotent
 not card A in omega ;
then A1: omega c= card A by CARD_1:4;
 card A c= omega by CARD_3:def_14;
then  card NAT = card A by A1, CARD_1:47, XBOOLE_0:def_10;
hence  NAT ,A are_equipotent by CARD_1:5; ::_thesis: verum
end;

theorem :: WAYBEL12:3
for L being non empty transitive RelStr
for A, B being Subset of L st A is_finer_than B holds
downarrow A c= downarrow B
proof
let L be non empty transitive RelStr ; ::_thesis: for A, B being Subset of L st A is_finer_than B holds
downarrow A c= downarrow B
let A, B be Subset of L; ::_thesis: ( A is_finer_than B implies downarrow A c= downarrow B )
assume A1: for a being Element of L st a in A holds
ex b being Element of L st
( b in B & b >= a ) ; :: according to YELLOW_4:def_1 ::_thesis: downarrow A c= downarrow B
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in downarrow A or q in downarrow B )
assume A2: q in downarrow A ; ::_thesis: q in downarrow B
then reconsider q1 = q as Element of L ;
consider a being Element of L such that
A3: a >= q1 and
A4: a in A by A2, WAYBEL_0:def_15;
consider b being Element of L such that
A5: b in B and
A6: b >= a by A1, A4;
 b >= q1 by A3, A6, ORDERS_2:3;
hence  q in downarrow B by A5, WAYBEL_0:def_15; ::_thesis: verum
end;

theorem Th4: :: WAYBEL12:4
for L being non empty transitive RelStr
for A, B being Subset of L st A is_coarser_than B holds
uparrow A c= uparrow B
proof
let L be non empty transitive RelStr ; ::_thesis: for A, B being Subset of L st A is_coarser_than B holds
uparrow A c= uparrow B
let A, B be Subset of L; ::_thesis: ( A is_coarser_than B implies uparrow A c= uparrow B )
assume A1: for a being Element of L st a in A holds
ex b being Element of L st
( b in B & b <= a ) ; :: according to YELLOW_4:def_2 ::_thesis: uparrow A c= uparrow B
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in uparrow A or q in uparrow B )
assume A2: q in uparrow A ; ::_thesis: q in uparrow B
then reconsider q1 = q as Element of L ;
consider a being Element of L such that
A3: a <= q1 and
A4: a in A by A2, WAYBEL_0:def_16;
consider b being Element of L such that
A5: b in B and
A6: b <= a by A1, A4;
 b <= q1 by A3, A6, ORDERS_2:3;
hence  q in uparrow B by A5, WAYBEL_0:def_16; ::_thesis: verum
end;

theorem :: WAYBEL12:5
for L being non empty Poset
for D being non empty finite filtered Subset of L st ex_inf_of D,L holds
inf D in D
proof
let L be non empty Poset; ::_thesis: for D being non empty finite filtered Subset of L st ex_inf_of D,L holds
inf D in D
let D be non empty finite filtered Subset of L; ::_thesis: ( ex_inf_of D,L implies inf D in D )
assume A1: ex_inf_of D,L ; ::_thesis: inf D in D
 D c= D ;
then consider d being Element of L such that
A2: d in D and
A3: d is_<=_than D by WAYBEL_0:2;
A4: inf D >= d by A1, A3, YELLOW_0:31;
 inf D is_<=_than D by A1, YELLOW_0:31;
then  inf D <= d by A2, LATTICE3:def_8;
hence  inf D in D by A2, A4, ORDERS_2:2; ::_thesis: verum
end;

theorem :: WAYBEL12:6
for L being non empty antisymmetric lower-bounded RelStr
for X being non empty lower Subset of L holds Bottom L in X
proof
let L be non empty antisymmetric lower-bounded RelStr ; ::_thesis: for X being non empty lower Subset of L holds Bottom L in X
let X be non empty lower Subset of L; ::_thesis: Bottom L in X
consider y being set  such that
A1: y in X by XBOOLE_0:def_1;
reconsider y = y as Element of X by A1;
 Bottom L <= y by YELLOW_0:44;
hence  Bottom L in X by WAYBEL_0:def_19; ::_thesis: verum
end;

theorem :: WAYBEL12:7
for L being non empty antisymmetric lower-bounded RelStr
for X being non empty Subset of L holds Bottom L in downarrow X
proof
let L be non empty antisymmetric lower-bounded RelStr ; ::_thesis: for X being non empty Subset of L holds Bottom L in downarrow X
let X be non empty Subset of L; ::_thesis: Bottom L in downarrow X
consider y being set  such that
A1: y in X by XBOOLE_0:def_1;
reconsider y = y as Element of X by A1;
 ( downarrow X =  {  x where x is Element of L : ex y being Element of L st
( x <= y & y in X )  }  & Bottom L <= y ) by WAYBEL_0:14, YELLOW_0:44;
hence  Bottom L in downarrow X ; ::_thesis: verum
end;

theorem Th8: :: WAYBEL12:8
for L being non empty antisymmetric upper-bounded RelStr
for X being non empty upper Subset of L holds Top L in X
proof
let L be non empty antisymmetric upper-bounded RelStr ; ::_thesis: for X being non empty upper Subset of L holds Top L in X
let X be non empty upper Subset of L; ::_thesis: Top L in X
consider y being set  such that
A1: y in X by XBOOLE_0:def_1;
reconsider y = y as Element of X by A1;
 Top L >= y by YELLOW_0:45;
hence  Top L in X by WAYBEL_0:def_20; ::_thesis: verum
end;

theorem Th9: :: WAYBEL12:9
for L being non empty antisymmetric upper-bounded RelStr
for X being non empty Subset of L holds Top L in uparrow X
proof
let L be non empty antisymmetric upper-bounded RelStr ; ::_thesis: for X being non empty Subset of L holds Top L in uparrow X
let X be non empty Subset of L; ::_thesis: Top L in uparrow X
consider y being set  such that
A1: y in X by XBOOLE_0:def_1;
reconsider y = y as Element of X by A1;
 ( uparrow X =  {  x where x is Element of L : ex y being Element of L st
( x >= y & y in X )  }  & Top L >= y ) by WAYBEL_0:15, YELLOW_0:45;
hence  Top L in uparrow X ; ::_thesis: verum
end;

theorem Th10: :: WAYBEL12:10
for L being antisymmetric lower-bounded with_infima RelStr
for X being Subset of L holds X "/\" {(Bottom L)} c= {(Bottom L)}
proof
let L be antisymmetric lower-bounded with_infima RelStr ; ::_thesis: for X being Subset of L holds X "/\" {(Bottom L)} c= {(Bottom L)}
let X be Subset of L; ::_thesis: X "/\" {(Bottom L)} c= {(Bottom L)}
A1: {(Bottom L)} "/\" X =  {  ((Bottom L) "/\" y) where y is Element of L : y in X  }  by YELLOW_4:42;
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in X "/\" {(Bottom L)} or q in {(Bottom L)} )
assume  q in X "/\" {(Bottom L)} ; ::_thesis: q in {(Bottom L)}
then consider y being Element of L such that
A2: q = (Bottom L) "/\" y and
 y in X by A1;
 y "/\" (Bottom L) = Bottom L by WAYBEL_1:3;
hence  q in {(Bottom L)} by A2, TARSKI:def_1; ::_thesis: verum
end;

theorem :: WAYBEL12:11
for L being antisymmetric lower-bounded with_infima RelStr
for X being non empty Subset of L holds X "/\" {(Bottom L)} = {(Bottom L)}
proof
let L be antisymmetric lower-bounded with_infima RelStr ; ::_thesis: for X being non empty Subset of L holds X "/\" {(Bottom L)} = {(Bottom L)}
let X be non empty Subset of L; ::_thesis: X "/\" {(Bottom L)} = {(Bottom L)}
thus  X "/\" {(Bottom L)} c= {(Bottom L)} by Th10; :: according to XBOOLE_0:def_10 ::_thesis: {(Bottom L)} c= X "/\" {(Bottom L)}
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in {(Bottom L)} or q in X "/\" {(Bottom L)} )
assume  q in {(Bottom L)} ; ::_thesis: q in X "/\" {(Bottom L)}
then A1: ( X "/\" {(Bottom L)} =  {  ((Bottom L) "/\" y) where y is Element of L : y in X  }  & q = Bottom L ) by TARSKI:def_1, YELLOW_4:42;
consider y being set  such that
A2: y in X by XBOOLE_0:def_1;
reconsider y = y as Element of X by A2;
 (Bottom L) "/\" y = Bottom L by WAYBEL_1:3;
hence  q in X "/\" {(Bottom L)} by A1; ::_thesis: verum
end;

theorem Th12: :: WAYBEL12:12
for L being antisymmetric upper-bounded with_suprema RelStr
for X being Subset of L holds X "\/" {(Top L)} c= {(Top L)}
proof
let L be antisymmetric upper-bounded with_suprema RelStr ; ::_thesis: for X being Subset of L holds X "\/" {(Top L)} c= {(Top L)}
let X be Subset of L; ::_thesis: X "\/" {(Top L)} c= {(Top L)}
A1: {(Top L)} "\/" X =  {  ((Top L) "\/" y) where y is Element of L : y in X  }  by YELLOW_4:15;
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in X "\/" {(Top L)} or q in {(Top L)} )
assume  q in X "\/" {(Top L)} ; ::_thesis: q in {(Top L)}
then consider y being Element of L such that
A2: q = (Top L) "\/" y and
 y in X by A1;
 y "\/" (Top L) = Top L by WAYBEL_1:4;
hence  q in {(Top L)} by A2, TARSKI:def_1; ::_thesis: verum
end;

theorem :: WAYBEL12:13
for L being antisymmetric upper-bounded with_suprema RelStr
for X being non empty Subset of L holds X "\/" {(Top L)} = {(Top L)}
proof
let L be antisymmetric upper-bounded with_suprema RelStr ; ::_thesis: for X being non empty Subset of L holds X "\/" {(Top L)} = {(Top L)}
let X be non empty Subset of L; ::_thesis: X "\/" {(Top L)} = {(Top L)}
thus  X "\/" {(Top L)} c= {(Top L)} by Th12; :: according to XBOOLE_0:def_10 ::_thesis: {(Top L)} c= X "\/" {(Top L)}
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in {(Top L)} or q in X "\/" {(Top L)} )
assume  q in {(Top L)} ; ::_thesis: q in X "\/" {(Top L)}
then A1: ( X "\/" {(Top L)} =  {  ((Top L) "\/" y) where y is Element of L : y in X  }  & q = Top L ) by TARSKI:def_1, YELLOW_4:15;
consider y being set  such that
A2: y in X by XBOOLE_0:def_1;
reconsider y = y as Element of X by A2;
 (Top L) "\/" y = Top L by WAYBEL_1:4;
hence  q in X "\/" {(Top L)} by A1; ::_thesis: verum
end;

theorem Th14: :: WAYBEL12:14
for L being upper-bounded Semilattice
for X being Subset of L holds {(Top L)} "/\" X = X
proof
let L be upper-bounded Semilattice; ::_thesis: for X being Subset of L holds {(Top L)} "/\" X = X
let X be Subset of L; ::_thesis: {(Top L)} "/\" X = X
A1: {(Top L)} "/\" X =  {  ((Top L) "/\" y) where y is Element of L : y in X  }  by YELLOW_4:42;
thus  {(Top L)} "/\" X c= X :: according to XBOOLE_0:def_10 ::_thesis: X c= {(Top L)} "/\" X
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in {(Top L)} "/\" X or q in X )
assume  q in {(Top L)} "/\" X ; ::_thesis: q in X
then  ex y being Element of L st
( q = (Top L) "/\" y & y in X ) by A1;
hence  q in X by WAYBEL_1:4; ::_thesis: verum
end;
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in X or q in {(Top L)} "/\" X )
assume A2: q in X ; ::_thesis: q in {(Top L)} "/\" X
then reconsider X1 = X as non empty Subset of L ;
reconsider y = q as Element of X1 by A2;
 q = (Top L) "/\" y by WAYBEL_1:4;
hence  q in {(Top L)} "/\" X by A1; ::_thesis: verum
end;

theorem :: WAYBEL12:15
for L being lower-bounded with_suprema Poset
for X being Subset of L holds {(Bottom L)} "\/" X = X
proof
let L be lower-bounded with_suprema Poset; ::_thesis: for X being Subset of L holds {(Bottom L)} "\/" X = X
let X be Subset of L; ::_thesis: {(Bottom L)} "\/" X = X
A1: {(Bottom L)} "\/" X =  {  ((Bottom L) "\/" y) where y is Element of L : y in X  }  by YELLOW_4:15;
thus  {(Bottom L)} "\/" X c= X :: according to XBOOLE_0:def_10 ::_thesis: X c= {(Bottom L)} "\/" X
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in {(Bottom L)} "\/" X or q in X )
assume  q in {(Bottom L)} "\/" X ; ::_thesis: q in X
then  ex y being Element of L st
( q = (Bottom L) "\/" y & y in X ) by A1;
hence  q in X by WAYBEL_1:3; ::_thesis: verum
end;
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in X or q in {(Bottom L)} "\/" X )
assume A2: q in X ; ::_thesis: q in {(Bottom L)} "\/" X
then reconsider X1 = X as non empty Subset of L ;
reconsider y = q as Element of X1 by A2;
 q = (Bottom L) "\/" y by WAYBEL_1:3;
hence  q in {(Bottom L)} "\/" X by A1; ::_thesis: verum
end;

theorem Th16: :: WAYBEL12:16
for L being non empty reflexive RelStr
for A, B being Subset of L st A c= B holds
( A is_finer_than B & A is_coarser_than B )
proof
let L be non empty reflexive RelStr ; ::_thesis: for A, B being Subset of L st A c= B holds
( A is_finer_than B & A is_coarser_than B )
let A, B be Subset of L; ::_thesis: ( A c= B implies ( A is_finer_than B & A is_coarser_than B ) )
assume A1: A c= B ; ::_thesis: ( A is_finer_than B & A is_coarser_than B )
thus  A is_finer_than B ::_thesis: A is_coarser_than B
proof
let a be Element of L; :: according to YELLOW_4:def_1 ::_thesis: ( not a in A or ex b1 being Element of the carrier of L st
( b1 in B & a <= b1 ) )
assume A2: a in A ; ::_thesis: ex b1 being Element of the carrier of L st
( b1 in B & a <= b1 )
take b = a; ::_thesis: ( b in B & a <= b )
thus  ( b in B & a <= b ) by A1, A2; ::_thesis: verum
end;
let a be Element of L; :: according to YELLOW_4:def_2 ::_thesis: ( not a in A or ex b1 being Element of the carrier of L st
( b1 in B & b1 <= a ) )
assume A3: a in A ; ::_thesis: ex b1 being Element of the carrier of L st
( b1 in B & b1 <= a )
take b = a; ::_thesis: ( b in B & b <= a )
thus  ( b in B & b <= a ) by A1, A3; ::_thesis: verum
end;

theorem Th17: :: WAYBEL12:17
for L being transitive antisymmetric with_infima RelStr
for V being Subset of L
for x, y being Element of L st x <= y holds
{y} "/\" V is_coarser_than {x} "/\" V
proof
let L be transitive antisymmetric with_infima RelStr ; ::_thesis: for V being Subset of L
for x, y being Element of L st x <= y holds
{y} "/\" V is_coarser_than {x} "/\" V
let V be Subset of L; ::_thesis: for x, y being Element of L st x <= y holds
{y} "/\" V is_coarser_than {x} "/\" V
let x, y be Element of L; ::_thesis: ( x <= y implies {y} "/\" V is_coarser_than {x} "/\" V )
assume A1: x <= y ; ::_thesis: {y} "/\" V is_coarser_than {x} "/\" V
A2: {y} "/\" V =  {  (y "/\" s) where s is Element of L : s in V  }  by YELLOW_4:42;
let b be Element of L; :: according to YELLOW_4:def_2 ::_thesis: ( not b in {y} "/\" V or ex b1 being Element of the carrier of L st
( b1 in {x} "/\" V & b1 <= b ) )
assume  b in {y} "/\" V ; ::_thesis: ex b1 being Element of the carrier of L st
( b1 in {x} "/\" V & b1 <= b )
then consider s being Element of L such that
A3: b = y "/\" s and
A4: s in V by A2;
take a = x "/\" s; ::_thesis: ( a in {x} "/\" V & a <= b )
 {x} "/\" V =  {  (x "/\" t) where t is Element of L : t in V  }  by YELLOW_4:42;
hence  a in {x} "/\" V by A4; ::_thesis: a <= b
thus  a <= b by A1, A3, WAYBEL_1:1; ::_thesis: verum
end;

theorem :: WAYBEL12:18
for L being transitive antisymmetric with_suprema RelStr
for V being Subset of L
for x, y being Element of L st x <= y holds
{x} "\/" V is_finer_than {y} "\/" V
proof
let L be transitive antisymmetric with_suprema RelStr ; ::_thesis: for V being Subset of L
for x, y being Element of L st x <= y holds
{x} "\/" V is_finer_than {y} "\/" V
let V be Subset of L; ::_thesis: for x, y being Element of L st x <= y holds
{x} "\/" V is_finer_than {y} "\/" V
let x, y be Element of L; ::_thesis: ( x <= y implies {x} "\/" V is_finer_than {y} "\/" V )
assume A1: x <= y ; ::_thesis: {x} "\/" V is_finer_than {y} "\/" V
A2: {x} "\/" V =  {  (x "\/" s) where s is Element of L : s in V  }  by YELLOW_4:15;
let b be Element of L; :: according to YELLOW_4:def_1 ::_thesis: ( not b in {x} "\/" V or ex b1 being Element of the carrier of L st
( b1 in {y} "\/" V & b <= b1 ) )
assume  b in {x} "\/" V ; ::_thesis: ex b1 being Element of the carrier of L st
( b1 in {y} "\/" V & b <= b1 )
then consider s being Element of L such that
A3: b = x "\/" s and
A4: s in V by A2;
take a = y "\/" s; ::_thesis: ( a in {y} "\/" V & b <= a )
 {y} "\/" V =  {  (y "\/" t) where t is Element of L : t in V  }  by YELLOW_4:15;
hence  a in {y} "\/" V by A4; ::_thesis: b <= a
thus  b <= a by A1, A3, WAYBEL_1:2; ::_thesis: verum
end;

theorem Th19: :: WAYBEL12:19
for L being non empty RelStr
for V, S, T being Subset of L st S is_coarser_than T & V is upper & T c= V holds
S c= V
proof
let L be non empty RelStr ; ::_thesis: for V, S, T being Subset of L st S is_coarser_than T & V is upper & T c= V holds
S c= V
let V, S, T be Subset of L; ::_thesis: ( S is_coarser_than T & V is upper & T c= V implies S c= V )
assume that
A1: S is_coarser_than T and
A2: ( V is upper & T c= V ) ; ::_thesis: S c= V
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in S or q in V )
assume A3: q in S ; ::_thesis: q in V
then reconsider S1 = S as non empty Subset of L ;
reconsider b = q as Element of S1 by A3;
 ex a being Element of L st
( a in T & a <= b ) by A1, YELLOW_4:def_2;
hence  q in V by A2, WAYBEL_0:def_20; ::_thesis: verum
end;

theorem :: WAYBEL12:20
for L being non empty RelStr
for V, S, T being Subset of L st S is_finer_than T & V is lower & T c= V holds
S c= V
proof
let L be non empty RelStr ; ::_thesis: for V, S, T being Subset of L st S is_finer_than T & V is lower & T c= V holds
S c= V
let V, S, T be Subset of L; ::_thesis: ( S is_finer_than T & V is lower & T c= V implies S c= V )
assume that
A1: S is_finer_than T and
A2: ( V is lower & T c= V ) ; ::_thesis: S c= V
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in S or q in V )
assume A3: q in S ; ::_thesis: q in V
then reconsider S1 = S as non empty Subset of L ;
reconsider a = q as Element of S1 by A3;
 ex b being Element of L st
( b in T & a <= b ) by A1, YELLOW_4:def_1;
hence  q in V by A2, WAYBEL_0:def_19; ::_thesis: verum
end;

theorem Th21: :: WAYBEL12:21
for L being Semilattice
for F being filtered upper Subset of L holds F "/\" F = F
proof
let L be Semilattice; ::_thesis: for F being filtered upper Subset of L holds F "/\" F = F
let F be filtered upper Subset of L; ::_thesis: F "/\" F = F
thus  F "/\" F c= F :: according to XBOOLE_0:def_10 ::_thesis: F c= F "/\" F
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F "/\" F or x in F )
assume  x in F "/\" F ; ::_thesis: x in F
then consider y, z being Element of L such that
A1: x = y "/\" z and
A2: ( y in F & z in F ) ;
consider t being Element of L such that
A3: t in F and
A4: ( t <= y & t <= z ) by A2, WAYBEL_0:def_2;
 y "/\" z >= t by A4, YELLOW_0:23;
hence  x in F by A1, A3, WAYBEL_0:def_20; ::_thesis: verum
end;
thus  F c= F "/\" F by YELLOW_4:40; ::_thesis: verum
end;

theorem :: WAYBEL12:22
for L being sup-Semilattice
for I being directed lower Subset of L holds I "\/" I = I
proof
let L be sup-Semilattice; ::_thesis: for I being directed lower Subset of L holds I "\/" I = I
let I be directed lower Subset of L; ::_thesis: I "\/" I = I
thus  I "\/" I c= I :: according to XBOOLE_0:def_10 ::_thesis: I c= I "\/" I
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in I "\/" I or x in I )
assume  x in I "\/" I ; ::_thesis: x in I
then consider y, z being Element of L such that
A1: x = y "\/" z and
A2: ( y in I & z in I ) ;
consider t being Element of L such that
A3: t in I and
A4: ( t >= y & t >= z ) by A2, WAYBEL_0:def_1;
 y "\/" z <= t by A4, YELLOW_0:22;
hence  x in I by A1, A3, WAYBEL_0:def_19; ::_thesis: verum
end;
thus  I c= I "\/" I by YELLOW_4:13; ::_thesis: verum
end;

Lm2:  for L being non empty RelStr
for V being Subset of L holds  {  x where x is Element of L : V "/\" {x} c= V  }  is Subset of L
proof
let L be non empty RelStr ; ::_thesis: for V being Subset of L holds  {  x where x is Element of L : V "/\" {x} c= V  }  is Subset of L
let V be Subset of L; ::_thesis:  {  x where x is Element of L : V "/\" {x} c= V  }  is Subset of L
set G =  {  x where x is Element of L : V "/\" {x} c= V  }  ;
  {  x where x is Element of L : V "/\" {x} c= V  }  c= the carrier of L
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in  {  x where x is Element of L : V "/\" {x} c= V  }  or q in the carrier of L )
assume  q in  {  x where x is Element of L : V "/\" {x} c= V  }  ; ::_thesis: q in the carrier of L
then  ex x being Element of L st
( q = x & V "/\" {x} c= V ) ;
hence  q in the carrier of L ; ::_thesis: verum
end;
hence   {  x where x is Element of L : V "/\" {x} c= V  }  is Subset of L ; ::_thesis: verum
end;

theorem Th23: :: WAYBEL12:23
for L being upper-bounded Semilattice
for V being Subset of L holds not  {  x where x is Element of L : V "/\" {x} c= V  }  is empty
proof
let L be upper-bounded Semilattice; ::_thesis: for V being Subset of L holds not  {  x where x is Element of L : V "/\" {x} c= V  }  is empty
let V be Subset of L; ::_thesis: not  {  x where x is Element of L : V "/\" {x} c= V  }  is empty
set G =  {  x where x is Element of L : V "/\" {x} c= V  }  ;
 V "/\" {(Top L)} = V by Th14;
then  Top L in  {  x where x is Element of L : V "/\" {x} c= V  }  ;
hence  not  {  x where x is Element of L : V "/\" {x} c= V  }  is empty ; ::_thesis: verum
end;

theorem Th24: :: WAYBEL12:24
for L being transitive antisymmetric with_infima RelStr
for V being Subset of L holds  {  x where x is Element of L : V "/\" {x} c= V  }  is filtered Subset of L
proof
let L be transitive antisymmetric with_infima RelStr ; ::_thesis: for V being Subset of L holds  {  x where x is Element of L : V "/\" {x} c= V  }  is filtered Subset of L
let V be Subset of L; ::_thesis:  {  x where x is Element of L : V "/\" {x} c= V  }  is filtered Subset of L
reconsider G1 =  {  x where x is Element of L : V "/\" {x} c= V  }  as Subset of L by Lm2;
 G1 is filtered
proof
let x, y be Element of L; :: according to WAYBEL_0:def_2 ::_thesis: ( not x in G1 or not y in G1 or ex b1 being Element of the carrier of L st
( b1 in G1 & b1 <= x & b1 <= y ) )
assume  x in G1 ; ::_thesis: ( not y in G1 or ex b1 being Element of the carrier of L st
( b1 in G1 & b1 <= x & b1 <= y ) )
then consider x1 being Element of L such that
A1: x = x1 and
A2: V "/\" {x1} c= V ;
assume  y in G1 ; ::_thesis: ex b1 being Element of the carrier of L st
( b1 in G1 & b1 <= x & b1 <= y )
then consider y1 being Element of L such that
A3: y = y1 and
A4: V "/\" {y1} c= V ;
take z = x1 "/\" y1; ::_thesis: ( z in G1 & z <= x & z <= y )
 V "/\" {z} c= V
proof
A5: {z} "/\" V =  {  (z "/\" v) where v is Element of L : v in V  }  by YELLOW_4:42;
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in V "/\" {z} or q in V )
assume  q in V "/\" {z} ; ::_thesis: q in V
then consider v being Element of L such that
A6: q = z "/\" v and
A7: v in V by A5;
A8: ( {x1} "/\" V =  {  (x1 "/\" s) where s is Element of L : s in V  }  & q = x1 "/\" (y1 "/\" v) ) by A6, LATTICE3:16, YELLOW_4:42;
 {y1} "/\" V =  {  (y1 "/\" t) where t is Element of L : t in V  }  by YELLOW_4:42;
then  y1 "/\" v in V "/\" {y1} by A7;
then  q in V "/\" {x1} by A4, A8;
hence  q in V by A2; ::_thesis: verum
end;
hence  z in G1 ; ::_thesis: ( z <= x & z <= y )
thus  ( z <= x & z <= y ) by A1, A3, YELLOW_0:23; ::_thesis: verum
end;
hence   {  x where x is Element of L : V "/\" {x} c= V  }  is filtered Subset of L ; ::_thesis: verum
end;

theorem Th25: :: WAYBEL12:25
for L being transitive antisymmetric with_infima RelStr
for V being upper Subset of L holds  {  x where x is Element of L : V "/\" {x} c= V  }  is upper Subset of L
proof
let L be transitive antisymmetric with_infima RelStr ; ::_thesis: for V being upper Subset of L holds  {  x where x is Element of L : V "/\" {x} c= V  }  is upper Subset of L
let V be upper Subset of L; ::_thesis:  {  x where x is Element of L : V "/\" {x} c= V  }  is upper Subset of L
reconsider G1 =  {  x where x is Element of L : V "/\" {x} c= V  }  as Subset of L by Lm2;
 G1 is upper
proof
let x, y be Element of L; :: according to WAYBEL_0:def_20 ::_thesis: ( not x in G1 or not x <= y or y in G1 )
assume  x in G1 ; ::_thesis: ( not x <= y or y in G1 )
then A1: ex x1 being Element of L st
( x1 = x & V "/\" {x1} c= V ) ;
assume  x <= y ; ::_thesis: y in G1
then  V "/\" {y} c= V by A1, Th17, Th19;
hence  y in G1 ; ::_thesis: verum
end;
hence   {  x where x is Element of L : V "/\" {x} c= V  }  is upper Subset of L ; ::_thesis: verum
end;

theorem Th26: :: WAYBEL12:26
for L being with_infima Poset
for X being Subset of L st X is Open & X is lower holds
X is filtered
proof
let L be with_infima Poset; ::_thesis: for X being Subset of L st X is Open & X is lower holds
X is filtered
let X be Subset of L; ::_thesis: ( X is Open & X is lower implies X is filtered )
assume A1: ( X is Open & X is lower ) ; ::_thesis: X is filtered
let x, y be Element of L; :: according to WAYBEL_0:def_2 ::_thesis: ( not x in X or not y in X or ex b1 being Element of the carrier of L st
( b1 in X & b1 <= x & b1 <= y ) )
assume that
A2: x in X and
 y in X ; ::_thesis: ex b1 being Element of the carrier of L st
( b1 in X & b1 <= x & b1 <= y )
A3: x "/\" y <= x by YELLOW_0:23;
then  x "/\" y in X by A1, A2, WAYBEL_0:def_19;
then consider z being Element of L such that
A4: z in X and
A5: z << x "/\" y by A1, WAYBEL_6:def_1;
take  z ; ::_thesis: ( z in X & z <= x & z <= y )
 ( x "/\" y <= y & z <= x "/\" y ) by A5, WAYBEL_3:1, YELLOW_0:23;
hence  ( z in X & z <= x & z <= y ) by A3, A4, ORDERS_2:3; ::_thesis: verum
end;

registration
let L be with_infima Poset;
cluster lower Open  ->  filtered for Element of bool the carrier of L;
coherence
 for b1 being Subset of L st b1 is Open & b1 is lower holds
b1 is filtered by Th26;
end;

registration
let L be non empty reflexive antisymmetric continuous RelStr ;
cluster lower  ->  Open for Element of bool the carrier of L;
coherence
 for b1 being Subset of L st b1 is lower holds
b1 is Open
proof
let A be Subset of L; ::_thesis: ( A is lower implies A is Open )
assume A1: A is lower ; ::_thesis: A is Open
let x be Element of L; :: according to WAYBEL_6:def_1 ::_thesis: ( not x in A or ex b1 being Element of the carrier of L st
( b1 in A & b1 is_way_below x ) )
assume A2: x in A ; ::_thesis: ex b1 being Element of the carrier of L st
( b1 in A & b1 is_way_below x )
consider y being set  such that
A3: y in waybelow x by XBOOLE_0:def_1;
reconsider y = y as Element of L by A3;
take  y ; ::_thesis: ( y in A & y is_way_below x )
 y << x by A3, WAYBEL_3:7;
then  y <= x by WAYBEL_3:1;
hence  ( y in A & y is_way_below x ) by A1, A2, A3, WAYBEL_0:def_19, WAYBEL_3:7; ::_thesis: verum
end;
end;

registration
let L be continuous Semilattice;
let x be Element of L;
cluster(downarrow x) `  ->  Open ;
coherence
 (downarrow x) ` is Open
proof
let a be Element of L; :: according to WAYBEL_6:def_1 ::_thesis: ( not a in (downarrow x) ` or ex b1 being Element of the carrier of L st
( b1 in (downarrow x) ` & b1 is_way_below a ) )
set A = (downarrow x) ` ;
assume  a in (downarrow x) ` ; ::_thesis: ex b1 being Element of the carrier of L st
( b1 in (downarrow x) ` & b1 is_way_below a )
then  not a in downarrow x by XBOOLE_0:def_5;
then A1: not a <= x by WAYBEL_0:17;
 for x being Element of L holds
( not waybelow x is empty & waybelow x is directed ) ;
then consider y being Element of L such that
A2: y << a and
A3: not y <= x by A1, WAYBEL_3:24;
take  y ; ::_thesis: ( y in (downarrow x) ` & y is_way_below a )
 not y in downarrow x by A3, WAYBEL_0:17;
hence  y in (downarrow x) ` by XBOOLE_0:def_5; ::_thesis: y is_way_below a
thus  y is_way_below a by A2; ::_thesis: verum
end;
end;

theorem Th27: :: WAYBEL12:27
for L being Semilattice
for C being non empty Subset of L st ( for x, y being Element of L st x in C & y in C & not x <= y holds
y <= x ) holds
for Y being non empty finite Subset of C holds "/\" (Y,L) in Y
proof
let L be Semilattice; ::_thesis: for C being non empty Subset of L st ( for x, y being Element of L st x in C & y in C & not x <= y holds
y <= x ) holds
for Y being non empty finite Subset of C holds "/\" (Y,L) in Y
let C be non empty Subset of L; ::_thesis: ( ( for x, y being Element of L st x in C & y in C & not x <= y holds
y <= x ) implies for Y being non empty finite Subset of C holds "/\" (Y,L) in Y )
assume A1: for x, y being Element of L st x in C & y in C & not x <= y holds
y <= x ; ::_thesis: for Y being non empty finite Subset of C holds "/\" (Y,L) in Y
defpred S1[ set ] means ( "/\" ($1,L) in $1 & ex_inf_of $1,L );
A2: for B1, B2 being non empty Element of Fin C st S1[B1] & S1[B2] holds
S1[B1 \/ B2]
proof
let B1, B2 be non empty Element of Fin C; ::_thesis: ( S1[B1] & S1[B2] implies S1[B1 \/ B2] )
assume A3: ( S1[B1] & S1[B2] ) ; ::_thesis: S1[B1 \/ B2]
 ( B1 c= C & B2 c= C ) by FINSUB_1:def_5;
then  ( "/\" (B1,L) <= "/\" (B2,L) or "/\" (B2,L) <= "/\" (B1,L) ) by A1, A3;
then A4: ( ("/\" (B1,L)) "/\" ("/\" (B2,L)) = "/\" (B1,L) or ("/\" (B1,L)) "/\" ("/\" (B2,L)) = "/\" (B2,L) ) by YELLOW_0:25;
 "/\" ((B1 \/ B2),L) = ("/\" (B1,L)) "/\" ("/\" (B2,L)) by A3, YELLOW_2:4;
hence  S1[B1 \/ B2] by A3, A4, XBOOLE_0:def_3, YELLOW_2:4; ::_thesis: verum
end;
let Y be non empty finite Subset of C; ::_thesis: "/\" (Y,L) in Y
A5: Y in Fin C by FINSUB_1:def_5;
A6: for x being Element of C holds S1[{x}]
proof
let x be Element of C; ::_thesis: S1[{x}]
 "/\" ({x},L) = x by YELLOW_0:39;
hence  S1[{x}] by TARSKI:def_1, YELLOW_0:38; ::_thesis: verum
end;
 for B being non empty Element of Fin C holds S1[B] from SETWISEO:sch_3(A6, A2);
hence  "/\" (Y,L) in Y by A5; ::_thesis: verum
end;

theorem :: WAYBEL12:28
for L being sup-Semilattice
for C being non empty Subset of L st ( for x, y being Element of L st x in C & y in C & not x <= y holds
y <= x ) holds
for Y being non empty finite Subset of C holds "\/" (Y,L) in Y
proof
let L be sup-Semilattice; ::_thesis: for C being non empty Subset of L st ( for x, y being Element of L st x in C & y in C & not x <= y holds
y <= x ) holds
for Y being non empty finite Subset of C holds "\/" (Y,L) in Y
let C be non empty Subset of L; ::_thesis: ( ( for x, y being Element of L st x in C & y in C & not x <= y holds
y <= x ) implies for Y being non empty finite Subset of C holds "\/" (Y,L) in Y )
assume A1: for x, y being Element of L st x in C & y in C & not x <= y holds
y <= x ; ::_thesis: for Y being non empty finite Subset of C holds "\/" (Y,L) in Y
defpred S1[ set ] means ( "\/" ($1,L) in $1 & ex_sup_of $1,L );
A2: for B1, B2 being non empty Element of Fin C st S1[B1] & S1[B2] holds
S1[B1 \/ B2]
proof
let B1, B2 be non empty Element of Fin C; ::_thesis: ( S1[B1] & S1[B2] implies S1[B1 \/ B2] )
assume A3: ( S1[B1] & S1[B2] ) ; ::_thesis: S1[B1 \/ B2]
 ( B1 c= C & B2 c= C ) by FINSUB_1:def_5;
then  ( "\/" (B1,L) <= "\/" (B2,L) or "\/" (B2,L) <= "\/" (B1,L) ) by A1, A3;
then A4: ( ("\/" (B1,L)) "\/" ("\/" (B2,L)) = "\/" (B1,L) or ("\/" (B1,L)) "\/" ("\/" (B2,L)) = "\/" (B2,L) ) by YELLOW_0:24;
 "\/" ((B1 \/ B2),L) = ("\/" (B1,L)) "\/" ("\/" (B2,L)) by A3, YELLOW_2:3;
hence  S1[B1 \/ B2] by A3, A4, XBOOLE_0:def_3, YELLOW_2:3; ::_thesis: verum
end;
let Y be non empty finite Subset of C; ::_thesis: "\/" (Y,L) in Y
A5: Y in Fin C by FINSUB_1:def_5;
A6: for x being Element of C holds S1[{x}]
proof
let x be Element of C; ::_thesis: S1[{x}]
 "\/" ({x},L) = x by YELLOW_0:39;
hence  S1[{x}] by TARSKI:def_1, YELLOW_0:38; ::_thesis: verum
end;
 for B being non empty Element of Fin C holds S1[B] from SETWISEO:sch_3(A6, A2);
hence  "\/" (Y,L) in Y by A5; ::_thesis: verum
end;

Lm3:  for L being Semilattice
for F being Filter of L holds F = uparrow (fininfs F)
proof
let L be Semilattice; ::_thesis: for F being Filter of L holds F = uparrow (fininfs F)
let F be Filter of L; ::_thesis: F = uparrow (fininfs F)
thus  F c= uparrow (fininfs F) by WAYBEL_0:62; :: according to XBOOLE_0:def_10 ::_thesis: uparrow (fininfs F) c= F
thus  uparrow (fininfs F) c= F by WAYBEL_0:62; ::_thesis: verum
end;

definition
let L be Semilattice;
let F be Filter of L;
mode GeneratorSet of F ->  Subset of L means :Def3: :: WAYBEL12:def 3
F = uparrow (fininfs it);
existence
 ex b1 being Subset of L st F = uparrow (fininfs b1)
proof
take  F ; ::_thesis: F = uparrow (fininfs F)
thus  F = uparrow (fininfs F) by Lm3; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines GeneratorSet WAYBEL12:def_3_:_
 for L being Semilattice
for F being Filter of L
for b3 being Subset of L holds
( b3 is GeneratorSet of F iff F = uparrow (fininfs b3) );

registration
let L be Semilattice;
let F be Filter of L;
cluster non empty for GeneratorSet of F;
existence
 not for b1 being GeneratorSet of F holds b1 is empty
proof
 F = uparrow (fininfs F) by Lm3;
then reconsider F1 = F as GeneratorSet of F by Def3;
take  F1 ; ::_thesis: not F1 is empty
thus  not F1 is empty ; ::_thesis: verum
end;
end;

Lm4:  for L being Semilattice
for F being Filter of L
for G being GeneratorSet of F holds G c= F
proof
let L be Semilattice; ::_thesis: for F being Filter of L
for G being GeneratorSet of F holds G c= F
let F be Filter of L; ::_thesis: for G being GeneratorSet of F holds G c= F
let G be GeneratorSet of F; ::_thesis: G c= F
 F = uparrow (fininfs G) by Def3;
hence  G c= F by WAYBEL_0:62; ::_thesis: verum
end;

theorem Th29: :: WAYBEL12:29
for L being Semilattice
for A being Subset of L
for B being non empty Subset of L st A is_coarser_than B holds
fininfs A is_coarser_than fininfs B
proof
let L be Semilattice; ::_thesis: for A being Subset of L
for B being non empty Subset of L st A is_coarser_than B holds
fininfs A is_coarser_than fininfs B
let A be Subset of L; ::_thesis: for B being non empty Subset of L st A is_coarser_than B holds
fininfs A is_coarser_than fininfs B
let B be non empty Subset of L; ::_thesis: ( A is_coarser_than B implies fininfs A is_coarser_than fininfs B )
assume A1: for a being Element of L st a in A holds
ex b being Element of L st
( b in B & b <= a ) ; :: according to YELLOW_4:def_2 ::_thesis: fininfs A is_coarser_than fininfs B
defpred S1[ set , set ] means  ex x, y being Element of L st
( x = $1 & y = $2 & y <= x );
let a be Element of L; :: according to YELLOW_4:def_2 ::_thesis: ( not a in fininfs A or ex b1 being Element of the carrier of L st
( b1 in fininfs B & b1 <= a ) )
assume  a in fininfs A ; ::_thesis: ex b1 being Element of the carrier of L st
( b1 in fininfs B & b1 <= a )
then consider Y being finite Subset of A such that
A2: a = "/\" (Y,L) and
A3: ex_inf_of Y,L ;
A4: for e being set st e in Y holds
ex u being set st
( u in B & S1[e,u] )
proof
let e be set ; ::_thesis: ( e in Y implies ex u being set st
( u in B & S1[e,u] ) )
assume A5: e in Y ; ::_thesis: ex u being set st
( u in B & S1[e,u] )
 Y c= the carrier of L by XBOOLE_1:1;
then reconsider e = e as Element of L by A5;
 ex b being Element of L st
( b in B & b <= e ) by A1, A5;
hence  ex u being set st
( u in B & S1[e,u] ) ; ::_thesis: verum
end;
consider f being Function of Y,B such that
A6: for e being set st e in Y holds
S1[e,f . e] from FUNCT_2:sch_1(A4);
A7: f .: Y c= the carrier of L
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in f .: Y or y in the carrier of L )
assume  y in f .: Y ; ::_thesis: y in the carrier of L
then consider x being set  such that
A8: x in dom f and
 x in Y and
A9: y = f . x by FUNCT_1:def_6;
 f . x in B by A8, FUNCT_2:5;
hence  y in the carrier of L by A9; ::_thesis: verum
end;
A10: now__::_thesis:_(_(_Y_=_{}_&_ex_inf_of_f_.:_Y,L_)_or_(_Y_<>_{}_&_ex_inf_of_f_.:_Y,L_)_)
percases ( Y = {} or Y <> {} ) ;
case Y = {} ; ::_thesis: ex_inf_of f .: Y,L
hence  ex_inf_of f .: Y,L by A3; ::_thesis: verum
end;
case Y <> {} ; ::_thesis: ex_inf_of f .: Y,L
then consider e being set  such that
A11: e in Y by XBOOLE_0:def_1;
 dom f = Y by FUNCT_2:def_1;
then  f . e in f .: Y by A11, FUNCT_1:def_6;
hence  ex_inf_of f .: Y,L by A7, YELLOW_0:55; ::_thesis: verum
end;
end;
end;
 "/\" ((f .: Y),L) is_<=_than Y
proof
let e be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not e in Y or "/\" ((f .: Y),L) <= e )
assume A12: e in Y ; ::_thesis: "/\" ((f .: Y),L) <= e
then consider x, y being Element of L such that
A13: x = e and
A14: y = f . e and
A15: y <= x by A6;
 dom f = Y by FUNCT_2:def_1;
then  f . e in f .: Y by A12, FUNCT_1:def_6;
then  "/\" ((f .: Y),L) <= y by A10, A14, YELLOW_4:2;
hence  "/\" ((f .: Y),L) <= e by A13, A15, ORDERS_2:3; ::_thesis: verum
end;
then A16: "/\" ((f .: Y),L) <= "/\" (Y,L) by A3, YELLOW_0:31;
 "/\" ((f .: Y),L) in fininfs B by A10;
hence  ex b being Element of L st
( b in fininfs B & b <= a ) by A2, A16; ::_thesis: verum
end;

theorem Th30: :: WAYBEL12:30
for L being Semilattice
for F being Filter of L
for G being GeneratorSet of F
for A being non empty Subset of L st G is_coarser_than A & A is_coarser_than F holds
A is GeneratorSet of F
proof
let L be Semilattice; ::_thesis: for F being Filter of L
for G being GeneratorSet of F
for A being non empty Subset of L st G is_coarser_than A & A is_coarser_than F holds
A is GeneratorSet of F
let F be Filter of L; ::_thesis: for G being GeneratorSet of F
for A being non empty Subset of L st G is_coarser_than A & A is_coarser_than F holds
A is GeneratorSet of F
let G be GeneratorSet of F; ::_thesis: for A being non empty Subset of L st G is_coarser_than A & A is_coarser_than F holds
A is GeneratorSet of F
let A be non empty Subset of L; ::_thesis: ( G is_coarser_than A & A is_coarser_than F implies A is GeneratorSet of F )
assume A1: G is_coarser_than A ; ::_thesis: ( not A is_coarser_than F or A is GeneratorSet of F )
assume A2: A is_coarser_than F ; ::_thesis: A is GeneratorSet of F
 F = uparrow (fininfs G) by Def3;
hence  F c= uparrow (fininfs A) by A1, Th4, Th29; :: according to XBOOLE_0:def_10,WAYBEL12:def_3 ::_thesis: uparrow (fininfs A) c= F
 A c= F by A2, YELLOW_4:8;
hence  uparrow (fininfs A) c= F by WAYBEL_0:62; ::_thesis: verum
end;

theorem Th31: :: WAYBEL12:31
for L being Semilattice
for A being Subset of L
for f, g being Function of NAT, the carrier of L st rng f = A & ( for n being Element of NAT holds g . n = "/\" ( {  (f . m) where m is Element of NAT : m <= n  }  ,L) ) holds
A is_coarser_than rng g
proof
let L be Semilattice; ::_thesis: for A being Subset of L
for f, g being Function of NAT, the carrier of L st rng f = A & ( for n being Element of NAT holds g . n = "/\" ( {  (f . m) where m is Element of NAT : m <= n  }  ,L) ) holds
A is_coarser_than rng g
let A be Subset of L; ::_thesis: for f, g being Function of NAT, the carrier of L st rng f = A & ( for n being Element of NAT holds g . n = "/\" ( {  (f . m) where m is Element of NAT : m <= n  }  ,L) ) holds
A is_coarser_than rng g
let f, g be Function of NAT, the carrier of L; ::_thesis: ( rng f = A & ( for n being Element of NAT holds g . n = "/\" ( {  (f . m) where m is Element of NAT : m <= n  }  ,L) ) implies A is_coarser_than rng g )
assume that
A1: rng f = A and
A2: for n being Element of NAT holds g . n = "/\" ( {  (f . m) where m is Element of NAT : m <= n  }  ,L) ; ::_thesis: A is_coarser_than rng g
let a be Element of L; :: according to YELLOW_4:def_2 ::_thesis: ( not a in A or ex b1 being Element of the carrier of L st
( b1 in rng g & b1 <= a ) )
assume  a in A ; ::_thesis: ex b1 being Element of the carrier of L st
( b1 in rng g & b1 <= a )
then consider n being set  such that
A3: n in dom f and
A4: f . n = a by A1, FUNCT_1:def_3;
reconsider n = n as Element of NAT by A3;
reconsider T =  {  (f . m) where m is Element of NAT : m <= n  }  as non empty finite Subset of L by Lm1;
take b = "/\" (T,L); ::_thesis: ( b in rng g & b <= a )
 ( dom g = NAT & g . n = b ) by A2, FUNCT_2:def_1;
hence  b in rng g by FUNCT_1:def_3; ::_thesis: b <= a
 f . n in T ;
then A5: {(f . n)} c= T by ZFMISC_1:31;
 ( ex_inf_of {(f . n)},L & ex_inf_of T,L ) by YELLOW_0:55;
then  b <= "/\" ({(f . n)},L) by A5, YELLOW_0:35;
hence  b <= a by A4, YELLOW_0:39; ::_thesis: verum
end;

theorem Th32: :: WAYBEL12:32
for L being Semilattice
for F being Filter of L
for G being GeneratorSet of F
for f, g being Function of NAT, the carrier of L st rng f = G & ( for n being Element of NAT holds g . n = "/\" ( {  (f . m) where m is Element of NAT : m <= n  }  ,L) ) holds
rng g is GeneratorSet of F
proof
let L be Semilattice; ::_thesis: for F being Filter of L
for G being GeneratorSet of F
for f, g being Function of NAT, the carrier of L st rng f = G & ( for n being Element of NAT holds g . n = "/\" ( {  (f . m) where m is Element of NAT : m <= n  }  ,L) ) holds
rng g is GeneratorSet of F
let F be Filter of L; ::_thesis: for G being GeneratorSet of F
for f, g being Function of NAT, the carrier of L st rng f = G & ( for n being Element of NAT holds g . n = "/\" ( {  (f . m) where m is Element of NAT : m <= n  }  ,L) ) holds
rng g is GeneratorSet of F
let G be GeneratorSet of F; ::_thesis: for f, g being Function of NAT, the carrier of L st rng f = G & ( for n being Element of NAT holds g . n = "/\" ( {  (f . m) where m is Element of NAT : m <= n  }  ,L) ) holds
rng g is GeneratorSet of F
let f, g be Function of NAT, the carrier of L; ::_thesis: ( rng f = G & ( for n being Element of NAT holds g . n = "/\" ( {  (f . m) where m is Element of NAT : m <= n  }  ,L) ) implies rng g is GeneratorSet of F )
assume that
A1: rng f = G and
A2: for n being Element of NAT holds g . n = "/\" ( {  (f . m) where m is Element of NAT : m <= n  }  ,L) ; ::_thesis: rng g is GeneratorSet of F
A3: rng g is_coarser_than F
proof
let a be Element of L; :: according to YELLOW_4:def_2 ::_thesis: ( not a in rng g or ex b1 being Element of the carrier of L st
( b1 in F & b1 <= a ) )
assume  a in rng g ; ::_thesis: ex b1 being Element of the carrier of L st
( b1 in F & b1 <= a )
then consider n being set  such that
A4: n in dom g and
A5: g . n = a by FUNCT_1:def_3;
reconsider n = n as Element of NAT by A4;
reconsider Y =  {  (f . m) where m is Element of NAT : m <= n  }  as non empty finite Subset of L by Lm1;
A6: Y c= G
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in Y or q in G )
assume  q in Y ; ::_thesis: q in G
then A7: ex m being Element of NAT st
( q = f . m & m <= n ) ;
 dom f = NAT by FUNCT_2:def_1;
hence  q in G by A1, A7, FUNCT_1:def_3; ::_thesis: verum
end;
 G c= F by Lm4;
then  Y c= F by A6, XBOOLE_1:1;
then A8: "/\" (Y,L) in F by WAYBEL_0:43;
 g . n = "/\" (Y,L) by A2;
hence  ex b being Element of L st
( b in F & b <= a ) by A5, A8; ::_thesis: verum
end;
 g . 0 in rng g by FUNCT_2:4;
hence  rng g is GeneratorSet of F by A1, A2, A3, Th30, Th31; ::_thesis: verum
end;

begin

theorem Th33: :: WAYBEL12:33
for L being lower-bounded continuous LATTICE
for V being upper Open Subset of L
for F being Filter of L
for v being Element of L st V "/\" F c= V & v in V & ex A being non empty GeneratorSet of F st A is countable holds
ex O being Open Filter of L st
( O c= V & v in O & F c= O )
proof
let L be lower-bounded continuous LATTICE; ::_thesis: for V being upper Open Subset of L
for F being Filter of L
for v being Element of L st V "/\" F c= V & v in V & ex A being non empty GeneratorSet of F st A is countable holds
ex O being Open Filter of L st
( O c= V & v in O & F c= O )
let V be upper Open Subset of L; ::_thesis: for F being Filter of L
for v being Element of L st V "/\" F c= V & v in V & ex A being non empty GeneratorSet of F st A is countable holds
ex O being Open Filter of L st
( O c= V & v in O & F c= O )
let F be Filter of L; ::_thesis: for v being Element of L st V "/\" F c= V & v in V & ex A being non empty GeneratorSet of F st A is countable holds
ex O being Open Filter of L st
( O c= V & v in O & F c= O )
let v be Element of L; ::_thesis: ( V "/\" F c= V & v in V & ex A being non empty GeneratorSet of F st A is countable implies ex O being Open Filter of L st
( O c= V & v in O & F c= O ) )
assume that
A1: V "/\" F c= V and
A2: v in V ; ::_thesis: ( for A being non empty GeneratorSet of F holds not A is countable or ex O being Open Filter of L st
( O c= V & v in O & F c= O ) )
reconsider V1 = V as non empty upper Open Subset of L by A2;
reconsider v1 = v as Element of V1 by A2;
reconsider G =  {  x where x is Element of L : V "/\" {x} c= V  }  as Filter of L by Th23, Th24, Th25;
given A being non empty GeneratorSet of F such that A3: A is countable ; ::_thesis: ex O being Open Filter of L st
( O c= V & v in O & F c= O )
consider f being Function of NAT,A such that
A4: rng f = A by A3, CARD_3:96;
reconsider f = f as Function of NAT, the carrier of L by FUNCT_2:7;
deffunc H1( Element of NAT ) ->  Element of the carrier of L = "/\" ( {  (f . m) where m is Element of NAT : m <= $1  }  ,L);
consider g being Function of NAT, the carrier of L such that
A5: for n being Element of NAT holds g . n = H1(n) from FUNCT_2:sch_4();
defpred S1[ Element of NAT , set , set ] means  ex x1, y1 being Element of V1 ex z1 being Element of L st
( x1 = $2 & y1 = $3 & z1 = g . ($1 + 1) & y1 << x1 "/\" z1 );
A6: dom g = NAT by FUNCT_2:def_1;
then reconsider AA = rng g as non empty Subset of L by RELAT_1:42;
A7: AA is GeneratorSet of F by A4, A5, Th32;
A8: F c= G
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in F or q in G )
assume A9: q in F ; ::_thesis: q in G
then reconsider s = q as Element of L ;
A10: V "/\" {s} =  {  (s "/\" t) where t is Element of L : t in V  }  by YELLOW_4:42;
 V "/\" {s} c= V
proof
let w be set ; :: according to TARSKI:def_3 ::_thesis: ( not w in V "/\" {s} or w in V )
assume  w in V "/\" {s} ; ::_thesis: w in V
then consider t being Element of L such that
A11: w = s "/\" t and
A12: t in V by A10;
 t "/\" s in V "/\" F by A9, A12;
hence  w in V by A1, A11; ::_thesis: verum
end;
hence  q in G ; ::_thesis: verum
end;
A13: for n being Element of NAT
for x being Element of V1 ex y being Element of V1 st S1[n,x,y]
proof
let n be Element of NAT ; ::_thesis: for x being Element of V1 ex y being Element of V1 st S1[n,x,y]
let x be Element of V1; ::_thesis: ex y being Element of V1 st S1[n,x,y]
 AA c= F by A7, Lm4;
then A14: AA c= G by A8, XBOOLE_1:1;
 g . (n + 1) in AA by A6, FUNCT_1:def_3;
then  g . (n + 1) in G by A14;
then consider g1 being Element of L such that
A15: g . (n + 1) = g1 and
A16: V "/\" {g1} c= V ;
 g1 in {g1} by TARSKI:def_1;
then  x "/\" g1 in V "/\" {g1} ;
then  ex y1 being Element of L st
( y1 in V & y1 << x "/\" g1 ) by A16, WAYBEL_6:def_1;
hence  ex y being Element of V1 st S1[n,x,y] by A15; ::_thesis: verum
end;
consider h being Function of NAT,V1 such that
A17: h . 0 = v1 and
A18: for n being Element of NAT holds S1[n,h . n,h . (n + 1)] from RECDEF_1:sch_2(A13);
A19: dom h = NAT by FUNCT_2:def_1;
then A20: h . 0 in rng h by FUNCT_1:def_3;
then reconsider R = rng h as non empty Subset of L by XBOOLE_1:1;
set O = uparrow (fininfs R);
A21: R c= uparrow (fininfs R) by WAYBEL_0:62;
A22: for x, y being Element of L
for n being Element of NAT st h . n = x & h . (n + 1) = y holds
y <= x
proof
let x, y be Element of L; ::_thesis: for n being Element of NAT st h . n = x & h . (n + 1) = y holds
y <= x
let n be Element of NAT ; ::_thesis: ( h . n = x & h . (n + 1) = y implies y <= x )
assume A23: ( h . n = x & h . (n + 1) = y ) ; ::_thesis: y <= x
consider x1, y1 being Element of V1, z1 being Element of L such that
A24: ( x1 = h . n & y1 = h . (n + 1) ) and
 z1 = g . (n + 1) and
A25: y1 << x1 "/\" z1 by A18;
A26: x1 "/\" z1 <= x1 by YELLOW_0:23;
 y1 <= x1 "/\" z1 by A25, WAYBEL_3:1;
hence  y <= x by A23, A24, A26, ORDERS_2:3; ::_thesis: verum
end;
A27: for x, y being Element of L
for n, m being Element of NAT st h . n = x & h . m = y & n <= m holds
y <= x
proof
defpred S2[ Element of NAT ] means  for a being Element of NAT
for s, t being Element of L st t = h . a & s = h . $1 & a <= $1 holds
s <= t;
A28: for k being Element of NAT st S2[k] holds
S2[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S2[k] implies S2[k + 1] )
assume A29: for j being Element of NAT
for s, t being Element of L st t = h . j & s = h . k & j <= k holds
s <= t ; ::_thesis: S2[k + 1]
 h . k in R by A19, FUNCT_1:def_3;
then reconsider s = h . k as Element of L ;
let a be Element of NAT ; ::_thesis: for s, t being Element of L st t = h . a & s = h . (k + 1) & a <= k + 1 holds
s <= t
let c, d be Element of L; ::_thesis: ( d = h . a & c = h . (k + 1) & a <= k + 1 implies c <= d )
assume that
A30: d = h . a and
A31: c = h . (k + 1) and
A32: a <= k + 1 ; ::_thesis: c <= d
A33: c <= s by A22, A31;
percases ( a <= k or a = k + 1 ) by A32, NAT_1:8;
suppose a <= k ; ::_thesis: c <= d
then  s <= d by A29, A30;
hence  c <= d by A33, ORDERS_2:3; ::_thesis: verum
end;
suppose a = k + 1 ; ::_thesis: c <= d
hence  c <= d by A30, A31; ::_thesis: verum
end;
end;
end;
A34: S2[ 0 ] by NAT_1:3;
A35: for k being Element of NAT holds S2[k] from NAT_1:sch_1(A34, A28);
let x, y be Element of L; ::_thesis: for n, m being Element of NAT st h . n = x & h . m = y & n <= m holds
y <= x
let n, m be Element of NAT ; ::_thesis: ( h . n = x & h . m = y & n <= m implies y <= x )
assume  ( h . n = x & h . m = y & n <= m ) ; ::_thesis: y <= x
hence  y <= x by A35; ::_thesis: verum
end;
A36: for x, y being Element of L st x in R & y in R & not x <= y holds
y <= x
proof
let x, y be Element of L; ::_thesis: ( x in R & y in R & not x <= y implies y <= x )
assume that
A37: x in R and
A38: y in R ; ::_thesis: ( x <= y or y <= x )
consider m being set  such that
A39: m in dom h and
A40: y = h . m by A38, FUNCT_1:def_3;
reconsider m = m as Element of NAT by A39;
consider n being set  such that
A41: n in dom h and
A42: x = h . n by A37, FUNCT_1:def_3;
reconsider n = n as Element of NAT by A41;
percases ( m <= n or n <= m ) ;
suppose m <= n ; ::_thesis: ( x <= y or y <= x )
hence  ( x <= y or y <= x ) by A27, A42, A40; ::_thesis: verum
end;
suppose n <= m ; ::_thesis: ( x <= y or y <= x )
hence  ( x <= y or y <= x ) by A27, A42, A40; ::_thesis: verum
end;
end;
end;
A43: uparrow (fininfs R) is Open
proof
let x be Element of L; :: according to WAYBEL_6:def_1 ::_thesis: ( not x in uparrow (fininfs R) or ex b1 being Element of the carrier of L st
( b1 in uparrow (fininfs R) & b1 is_way_below x ) )
assume  x in uparrow (fininfs R) ; ::_thesis: ex b1 being Element of the carrier of L st
( b1 in uparrow (fininfs R) & b1 is_way_below x )
then consider y being Element of L such that
A44: y <= x and
A45: y in fininfs R by WAYBEL_0:def_16;
consider Y being finite Subset of R such that
A46: y = "/\" (Y,L) and
 ex_inf_of Y,L by A45;
percases ( Y <> {} or Y = {} ) ;
suppose Y <> {} ; ::_thesis: ex b1 being Element of the carrier of L st
( b1 in uparrow (fininfs R) & b1 is_way_below x )
then  y in Y by A36, A46, Th27;
then consider n being set  such that
A47: n in dom h and
A48: h . n = y by FUNCT_1:def_3;
reconsider n = n as Element of NAT by A47;
consider x1, y1 being Element of V1, z1 being Element of L such that
A49: x1 = h . n and
A50: y1 = h . (n + 1) and
 z1 = g . (n + 1) and
A51: y1 << x1 "/\" z1 by A18;
take  y1 ; ::_thesis: ( y1 in uparrow (fininfs R) & y1 is_way_below x )
 y1 in R by A19, A50, FUNCT_1:def_3;
hence  y1 in uparrow (fininfs R) by A21; ::_thesis: y1 is_way_below x
 x1 "/\" z1 <= x1 by YELLOW_0:23;
then  y1 << x1 by A51, WAYBEL_3:2;
hence  y1 is_way_below x by A44, A48, A49, WAYBEL_3:2; ::_thesis: verum
end;
supposeA52: Y = {} ; ::_thesis: ex b1 being Element of the carrier of L st
( b1 in uparrow (fininfs R) & b1 is_way_below x )
consider b being set  such that
A53: b in R by XBOOLE_0:def_1;
reconsider b = b as Element of L by A53;
consider n being set  such that
A54: n in dom h and
 h . n = b by A53, FUNCT_1:def_3;
reconsider n = n as Element of NAT by A54;
A55: x <= Top L by YELLOW_0:45;
consider x1, y1 being Element of V1, z1 being Element of L such that
 x1 = h . n and
A56: y1 = h . (n + 1) and
 z1 = g . (n + 1) and
A57: y1 << x1 "/\" z1 by A18;
 y = Top L by A46, A52, YELLOW_0:def_12;
then  x = Top L by A44, A55, ORDERS_2:2;
then A58: x1 <= x by YELLOW_0:45;
take  y1 ; ::_thesis: ( y1 in uparrow (fininfs R) & y1 is_way_below x )
 y1 in R by A19, A56, FUNCT_1:def_3;
hence  y1 in uparrow (fininfs R) by A21; ::_thesis: y1 is_way_below x
 x1 "/\" z1 <= x1 by YELLOW_0:23;
then  y1 << x1 by A57, WAYBEL_3:2;
hence  y1 is_way_below x by A58, WAYBEL_3:2; ::_thesis: verum
end;
end;
end;
A59: for n being Element of NAT
for a, b being Element of L st a = g . n & b = g . (n + 1) holds
b <= a
proof
let n be Element of NAT ; ::_thesis: for a, b being Element of L st a = g . n & b = g . (n + 1) holds
b <= a
let a, b be Element of L; ::_thesis: ( a = g . n & b = g . (n + 1) implies b <= a )
assume A60: ( a = g . n & b = g . (n + 1) ) ; ::_thesis: b <= a
reconsider gn =  {  (f . m) where m is Element of NAT : m <= n  }  , gn1 =  {  (f . k) where k is Element of NAT : k <= n + 1  }  as non empty finite Subset of L by Lm1;
A61: ( ex_inf_of gn,L & ex_inf_of gn1,L ) by YELLOW_0:55;
A62: gn c= gn1
proof
let i be set ; :: according to TARSKI:def_3 ::_thesis: ( not i in gn or i in gn1 )
assume  i in gn ; ::_thesis: i in gn1
then consider k being Element of NAT  such that
A63: i = f . k and
A64: k <= n ;
 k <= n + 1 by A64, NAT_1:12;
hence  i in gn1 by A63; ::_thesis: verum
end;
 ( a = "/\" (gn,L) & b = "/\" (gn1,L) ) by A5, A60;
hence  b <= a by A61, A62, YELLOW_0:35; ::_thesis: verum
end;
A65: AA is_coarser_than R
proof
let a be Element of L; :: according to YELLOW_4:def_2 ::_thesis: ( not a in AA or ex b1 being Element of the carrier of L st
( b1 in R & b1 <= a ) )
assume  a in AA ; ::_thesis: ex b1 being Element of the carrier of L st
( b1 in R & b1 <= a )
then consider x being set  such that
A66: x in dom g and
A67: g . x = a by FUNCT_1:def_3;
reconsider x = x as Element of NAT by A66;
consider x1, y1 being Element of V1, z1 being Element of L such that
 x1 = h . x and
A68: y1 = h . (x + 1) and
A69: z1 = g . (x + 1) and
A70: y1 << x1 "/\" z1 by A18;
 ( x1 "/\" z1 <= z1 & y1 <= x1 "/\" z1 ) by A70, WAYBEL_3:1, YELLOW_0:23;
then A71: y1 <= z1 by ORDERS_2:3;
A72: h . (x + 1) in R by A19, FUNCT_1:def_3;
 z1 <= a by A59, A67, A69;
hence  ex b being Element of L st
( b in R & b <= a ) by A68, A72, A71, ORDERS_2:3; ::_thesis: verum
end;
reconsider O = uparrow (fininfs R) as Open Filter of L by A43;
 R is_coarser_than O by A21, Th16;
then A73: AA c= O by A65, YELLOW_4:7, YELLOW_4:8;
take  O ; ::_thesis: ( O c= V & v in O & F c= O )
thus  O c= V ::_thesis: ( v in O & F c= O )
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in O or q in V )
assume  q in O ; ::_thesis: q in V
then reconsider q = q as Element of O ;
consider y being Element of L such that
A74: y <= q and
A75: y in fininfs R by WAYBEL_0:def_16;
consider Y being finite Subset of R such that
A76: y = "/\" (Y,L) and
 ex_inf_of Y,L by A75;
percases ( Y <> {} or Y = {} ) ;
suppose Y <> {} ; ::_thesis: q in V
then  y in Y by A36, A76, Th27;
then consider n being set  such that
A77: n in dom h and
A78: h . n = y by FUNCT_1:def_3;
reconsider n = n as Element of NAT by A77;
 ex x1, y1 being Element of V1 ex z1 being Element of L st
( x1 = h . n & y1 = h . (n + 1) & z1 = g . (n + 1) & y1 << x1 "/\" z1 ) by A18;
hence  q in V by A74, A78, WAYBEL_0:def_20; ::_thesis: verum
end;
supposeA79: Y = {} ; ::_thesis: q in V
A80: q <= Top L by YELLOW_0:45;
 y = Top L by A76, A79, YELLOW_0:def_12;
then  q = Top L by A74, A80, ORDERS_2:2;
hence  q in V by Th8; ::_thesis: verum
end;
end;
end;
thus  v in O by A17, A20, A21; ::_thesis: F c= O
 uparrow (fininfs AA) = F by A7, Def3;
hence  F c= O by A73, WAYBEL_0:62; ::_thesis: verum
end;

theorem Th34: :: WAYBEL12:34
for L being lower-bounded continuous LATTICE
for V being upper Open Subset of L
for N being non empty countable Subset of L
for v being Element of L st V "/\" N c= V & v in V holds
ex O being Open Filter of L st
( {v} "/\" N c= O & O c= V & v in O )
proof
let L be lower-bounded continuous LATTICE; ::_thesis: for V being upper Open Subset of L
for N being non empty countable Subset of L
for v being Element of L st V "/\" N c= V & v in V holds
ex O being Open Filter of L st
( {v} "/\" N c= O & O c= V & v in O )
let V be upper Open Subset of L; ::_thesis: for N being non empty countable Subset of L
for v being Element of L st V "/\" N c= V & v in V holds
ex O being Open Filter of L st
( {v} "/\" N c= O & O c= V & v in O )
let N be non empty countable Subset of L; ::_thesis: for v being Element of L st V "/\" N c= V & v in V holds
ex O being Open Filter of L st
( {v} "/\" N c= O & O c= V & v in O )
let v be Element of L; ::_thesis: ( V "/\" N c= V & v in V implies ex O being Open Filter of L st
( {v} "/\" N c= O & O c= V & v in O ) )
assume that
A1: V "/\" N c= V and
A2: v in V ; ::_thesis: ex O being Open Filter of L st
( {v} "/\" N c= O & O c= V & v in O )
reconsider G =  {  x where x is Element of L : V "/\" {x} c= V  }  as Filter of L by Th23, Th24, Th25;
A3: N c= G
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in N or q in G )
assume A4: q in N ; ::_thesis: q in G
then reconsider q1 = q as Element of L ;
A5: {q1} "/\" V =  {  (q1 "/\" y) where y is Element of L : y in V  }  by YELLOW_4:42;
 V "/\" {q1} c= V
proof
let t be set ; :: according to TARSKI:def_3 ::_thesis: ( not t in V "/\" {q1} or t in V )
assume  t in V "/\" {q1} ; ::_thesis: t in V
then consider y being Element of L such that
A6: t = q1 "/\" y and
A7: y in V by A5;
 q1 "/\" y in N "/\" V by A4, A7;
hence  t in V by A1, A6; ::_thesis: verum
end;
hence  q in G ; ::_thesis: verum
end;
 N is GeneratorSet of uparrow (fininfs N) by Def3;
then consider F being Filter of L such that
A8: N is GeneratorSet of F ;
 F = uparrow (fininfs N) by A8, Def3;
then A9: F c= G by A3, WAYBEL_0:62;
 V "/\" F c= V
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in V "/\" F or q in V )
assume  q in V "/\" F ; ::_thesis: q in V
then consider d, f being Element of L such that
A10: q = d "/\" f and
A11: d in V and
A12: f in F ;
 f in G by A9, A12;
then consider x being Element of L such that
A13: f = x and
A14: V "/\" {x} c= V ;
 x in {x} by TARSKI:def_1;
then  d "/\" f in V "/\" {x} by A11, A13;
hence  q in V by A10, A14; ::_thesis: verum
end;
then consider O being Open Filter of L such that
A15: O c= V and
A16: v in O and
A17: F c= O by A2, A8, Th33;
take  O ; ::_thesis: ( {v} "/\" N c= O & O c= V & v in O )
A18: {v} "/\" N =  {  (v "/\" n) where n is Element of L : n in N  }  by YELLOW_4:42;
thus  {v} "/\" N c= O ::_thesis: ( O c= V & v in O )
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in {v} "/\" N or q in O )
assume  q in {v} "/\" N ; ::_thesis: q in O
then consider n being Element of L such that
A19: q = v "/\" n and
A20: n in N by A18;
 N c= F by A8, Lm4;
then  N c= O by A17, XBOOLE_1:1;
then  v "/\" n in O "/\" O by A16, A20;
hence  q in O by A19, Th21; ::_thesis: verum
end;
thus  ( O c= V & v in O ) by A15, A16; ::_thesis: verum
end;

theorem Th35: :: WAYBEL12:35
for L being lower-bounded continuous LATTICE
for V being upper Open Subset of L
for N being non empty countable Subset of L
for x, y being Element of L st V "/\" N c= V & y in V & not x in V holds
ex p being irreducible Element of L st
( x <= p & not p in uparrow ({y} "/\" N) )
proof
let L be lower-bounded continuous LATTICE; ::_thesis: for V being upper Open Subset of L
for N being non empty countable Subset of L
for x, y being Element of L st V "/\" N c= V & y in V & not x in V holds
ex p being irreducible Element of L st
( x <= p & not p in uparrow ({y} "/\" N) )
let V be upper Open Subset of L; ::_thesis: for N being non empty countable Subset of L
for x, y being Element of L st V "/\" N c= V & y in V & not x in V holds
ex p being irreducible Element of L st
( x <= p & not p in uparrow ({y} "/\" N) )
let N be non empty countable Subset of L; ::_thesis: for x, y being Element of L st V "/\" N c= V & y in V & not x in V holds
ex p being irreducible Element of L st
( x <= p & not p in uparrow ({y} "/\" N) )
let x, y be Element of L; ::_thesis: ( V "/\" N c= V & y in V & not x in V implies ex p being irreducible Element of L st
( x <= p & not p in uparrow ({y} "/\" N) ) )
assume that
A1: ( V "/\" N c= V & y in V ) and
A2: not x in V ; ::_thesis: ex p being irreducible Element of L st
( x <= p & not p in uparrow ({y} "/\" N) )
consider O being Open Filter of L such that
A3: {y} "/\" N c= O and
A4: O c= V and
 y in O by A1, Th34;
 ( uparrow O c= O & O c= uparrow O ) by WAYBEL_0:16, WAYBEL_0:24;
then  uparrow O = O by XBOOLE_0:def_10;
then A5: uparrow ({y} "/\" N) c= O by A3, YELLOW_3:7;
 not x in O by A2, A4;
then  x in O ` by XBOOLE_0:def_5;
then consider p being Element of L such that
A6: x <= p and
A7: p is_maximal_in O ` by WAYBEL_6:9;
reconsider p = p as irreducible Element of L by A7, WAYBEL_6:13;
take  p ; ::_thesis: ( x <= p & not p in uparrow ({y} "/\" N) )
thus  x <= p by A6; ::_thesis: not p in uparrow ({y} "/\" N)
 p in O ` by A7, WAYBEL_4:55;
hence  not p in uparrow ({y} "/\" N) by A5, XBOOLE_0:def_5; ::_thesis: verum
end;

theorem Th36: :: WAYBEL12:36
for L being lower-bounded continuous LATTICE
for x being Element of L
for N being non empty countable Subset of L st ( for n, y being Element of L st not y <= x & n in N holds
not y "/\" n <= x ) holds
for y being Element of L st not y <= x holds
ex p being irreducible Element of L st
( x <= p & not p in uparrow ({y} "/\" N) )
proof
let L be lower-bounded continuous LATTICE; ::_thesis: for x being Element of L
for N being non empty countable Subset of L st ( for n, y being Element of L st not y <= x & n in N holds
not y "/\" n <= x ) holds
for y being Element of L st not y <= x holds
ex p being irreducible Element of L st
( x <= p & not p in uparrow ({y} "/\" N) )
let x be Element of L; ::_thesis: for N being non empty countable Subset of L st ( for n, y being Element of L st not y <= x & n in N holds
not y "/\" n <= x ) holds
for y being Element of L st not y <= x holds
ex p being irreducible Element of L st
( x <= p & not p in uparrow ({y} "/\" N) )
let N be non empty countable Subset of L; ::_thesis: ( ( for n, y being Element of L st not y <= x & n in N holds
not y "/\" n <= x ) implies for y being Element of L st not y <= x holds
ex p being irreducible Element of L st
( x <= p & not p in uparrow ({y} "/\" N) ) )
assume A1: for n, y being Element of L st not y <= x & n in N holds
not y "/\" n <= x ; ::_thesis: for y being Element of L st not y <= x holds
ex p being irreducible Element of L st
( x <= p & not p in uparrow ({y} "/\" N) )
set V = (downarrow x) ` ;
A2: ((downarrow x) `) "/\" N c= (downarrow x) `
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in ((downarrow x) `) "/\" N or q in (downarrow x) ` )
assume  q in ((downarrow x) `) "/\" N ; ::_thesis: q in (downarrow x) `
then consider v, n being Element of L such that
A3: q = v "/\" n and
A4: v in (downarrow x) ` and
A5: n in N ;
 not v in downarrow x by A4, XBOOLE_0:def_5;
then  not v <= x by WAYBEL_0:17;
then  not v "/\" n <= x by A1, A5;
then  not v "/\" n in downarrow x by WAYBEL_0:17;
hence  q in (downarrow x) ` by A3, XBOOLE_0:def_5; ::_thesis: verum
end;
 x <= x ;
then  x in downarrow x by WAYBEL_0:17;
then A6: not x in (downarrow x) ` by XBOOLE_0:def_5;
let y be Element of L; ::_thesis: ( not y <= x implies ex p being irreducible Element of L st
( x <= p & not p in uparrow ({y} "/\" N) ) )
assume  not y <= x ; ::_thesis: ex p being irreducible Element of L st
( x <= p & not p in uparrow ({y} "/\" N) )
then  not y in downarrow x by WAYBEL_0:17;
then  y in (downarrow x) ` by XBOOLE_0:def_5;
hence  ex p being irreducible Element of L st
( x <= p & not p in uparrow ({y} "/\" N) ) by A2, A6, Th35; ::_thesis: verum
end;

definition
let L be non empty RelStr ;
let u be Element of L;
attru is dense  means :Def4: :: WAYBEL12:def 4
 for v being Element of L st v <> Bottom L holds
u "/\" v <> Bottom L;
end;

:: deftheorem Def4 defines dense WAYBEL12:def_4_:_
 for L being non empty RelStr
for u being Element of L holds
( u is dense iff for v being Element of L st v <> Bottom L holds
u "/\" v <> Bottom L );

registration
let L be upper-bounded Semilattice;
cluster Top L ->  dense ;
coherence
 Top L is dense
proof
let v be Element of L; :: according to WAYBEL12:def_4 ::_thesis: ( v <> Bottom L implies (Top L) "/\" v <> Bottom L )
assume  v <> Bottom L ; ::_thesis: (Top L) "/\" v <> Bottom L
hence  (Top L) "/\" v <> Bottom L by WAYBEL_1:4; ::_thesis: verum
end;
end;

registration
let L be upper-bounded Semilattice;
cluster dense for Element of the carrier of L;
existence
 ex b1 being Element of L st b1 is dense
proof
take  Top L ; ::_thesis: Top L is dense
thus  Top L is dense ; ::_thesis: verum
end;
end;

theorem :: WAYBEL12:37
for L being non trivial bounded Semilattice
for x being Element of L st x is dense holds
x <> Bottom L
proof
let L be non trivial bounded Semilattice; ::_thesis: for x being Element of L st x is dense holds
x <> Bottom L
let x be Element of L; ::_thesis: ( x is dense implies x <> Bottom L )
assume A1: x is dense ; ::_thesis: x <> Bottom L
 Top L <> Bottom L by WAYBEL_7:3;
then  x "/\" (Top L) <> Bottom L by A1, Def4;
hence  x <> Bottom L by WAYBEL_1:4; ::_thesis: verum
end;

definition
let L be non empty RelStr ;
let D be Subset of L;
attrD is dense  means :Def5: :: WAYBEL12:def 5
 for d being Element of L st d in D holds
d is dense ;
end;

:: deftheorem Def5 defines dense WAYBEL12:def_5_:_
 for L being non empty RelStr
for D being Subset of L holds
( D is dense iff for d being Element of L st d in D holds
d is dense );

theorem Th38: :: WAYBEL12:38
for L being upper-bounded Semilattice holds {(Top L)} is dense
proof
let L be upper-bounded Semilattice; ::_thesis: {(Top L)} is dense
let d be Element of L; :: according to WAYBEL12:def_5 ::_thesis: ( d in {(Top L)} implies d is dense )
assume  d in {(Top L)} ; ::_thesis: d is dense
hence  d is dense by TARSKI:def_1; ::_thesis: verum
end;

registration
let L be upper-bounded Semilattice;
cluster non empty finite countable dense for Element of bool the carrier of L;
existence
 ex b1 being Subset of L st
( not b1 is empty & b1 is finite & b1 is countable & b1 is dense )
proof
take  {(Top L)} ; ::_thesis: ( not {(Top L)} is empty & {(Top L)} is finite & {(Top L)} is countable & {(Top L)} is dense )
thus  ( not {(Top L)} is empty & {(Top L)} is finite & {(Top L)} is countable ) ; ::_thesis: {(Top L)} is dense
thus  {(Top L)} is dense by Th38; ::_thesis: verum
end;
end;

theorem Th39: :: WAYBEL12:39
for L being lower-bounded continuous LATTICE
for D being non empty countable dense Subset of L
for u being Element of L st u <> Bottom L holds
ex p being irreducible Element of L st
( p <> Top L & not p in uparrow ({u} "/\" D) )
proof
let L be lower-bounded continuous LATTICE; ::_thesis: for D being non empty countable dense Subset of L
for u being Element of L st u <> Bottom L holds
ex p being irreducible Element of L st
( p <> Top L & not p in uparrow ({u} "/\" D) )
let D be non empty countable dense Subset of L; ::_thesis: for u being Element of L st u <> Bottom L holds
ex p being irreducible Element of L st
( p <> Top L & not p in uparrow ({u} "/\" D) )
let u be Element of L; ::_thesis: ( u <> Bottom L implies ex p being irreducible Element of L st
( p <> Top L & not p in uparrow ({u} "/\" D) ) )
assume A1: u <> Bottom L ; ::_thesis: ex p being irreducible Element of L st
( p <> Top L & not p in uparrow ({u} "/\" D) )
A2: for d, y being Element of L st not y <= Bottom L & d in D holds
not y "/\" d <= Bottom L
proof
let d, y be Element of L; ::_thesis: ( not y <= Bottom L & d in D implies not y "/\" d <= Bottom L )
assume A3: not y <= Bottom L ; ::_thesis: ( not d in D or not y "/\" d <= Bottom L )
assume  d in D ; ::_thesis: not y "/\" d <= Bottom L
then  d is dense by Def5;
then A4: y "/\" d <> Bottom L by A3, Def4;
 Bottom L <= y "/\" d by YELLOW_0:44;
hence  not y "/\" d <= Bottom L by A4, ORDERS_2:2; ::_thesis: verum
end;
 Bottom L <= u by YELLOW_0:44;
then  not u <= Bottom L by A1, ORDERS_2:2;
then consider p being irreducible Element of L such that
 Bottom L <= p and
A5: not p in uparrow ({u} "/\" D) by A2, Th36;
take  p ; ::_thesis: ( p <> Top L & not p in uparrow ({u} "/\" D) )
thus  p <> Top L by A5, Th9; ::_thesis: not p in uparrow ({u} "/\" D)
thus  not p in uparrow ({u} "/\" D) by A5; ::_thesis: verum
end;

theorem Th40: :: WAYBEL12:40
for T being non empty TopSpace
for A being Element of (InclPoset the topology of T)
for B being Subset of T st A = B & B ` is irreducible holds
A is irreducible
proof
let T be non empty TopSpace; ::_thesis: for A being Element of (InclPoset the topology of T)
for B being Subset of T st A = B & B ` is irreducible holds
A is irreducible
let A be Element of (InclPoset the topology of T); ::_thesis: for B being Subset of T st A = B & B ` is irreducible holds
A is irreducible
let B be Subset of T; ::_thesis: ( A = B & B ` is irreducible implies A is irreducible )
assume A1: A = B ; ::_thesis: ( not B ` is irreducible or A is irreducible )
assume that
 ( not B ` is empty & B ` is closed ) and
A2: for S1, S2 being Subset of T st S1 is closed & S2 is closed & B ` = S1 \/ S2 & not S1 = B ` holds
S2 = B ` ; :: according to YELLOW_8:def_3 ::_thesis: A is irreducible
let x, y be Element of (InclPoset the topology of T); :: according to WAYBEL_6:def_2 ::_thesis: ( not A = x "/\" y or x = A or y = A )
assume A3: A = x "/\" y ; ::_thesis: ( x = A or y = A )
A4: the carrier of (InclPoset the topology of T) = the topology of T by YELLOW_1:1;
then  ( x in the topology of T & y in the topology of T ) ;
then reconsider x1 = x, y1 = y as Subset of T ;
A5: y1 is open by A4, PRE_TOPC:def_2;
then A6: y1 ` is closed ;
A7: x1 is open by A4, PRE_TOPC:def_2;
then  x1 /\ y1 is open by A5;
then  x /\ y in the topology of T by PRE_TOPC:def_2;
then  A = x /\ y by A3, YELLOW_1:9;
then A8: B ` = (x1 `) \/ (y1 `) by A1, XBOOLE_1:54;
 x1 ` is closed by A7;
then  ( x1 ` = B ` or y1 ` = B ` ) by A2, A6, A8;
hence  ( x = A or y = A ) by A1, TOPS_1:1; ::_thesis: verum
end;

theorem Th41: :: WAYBEL12:41
for T being non empty TopSpace
for A being Element of (InclPoset the topology of T)
for B being Subset of T st A = B & A <> Top (InclPoset the topology of T) holds
( A is irreducible iff B ` is irreducible )
proof
let T be non empty TopSpace; ::_thesis: for A being Element of (InclPoset the topology of T)
for B being Subset of T st A = B & A <> Top (InclPoset the topology of T) holds
( A is irreducible iff B ` is irreducible )
let A be Element of (InclPoset the topology of T); ::_thesis: for B being Subset of T st A = B & A <> Top (InclPoset the topology of T) holds
( A is irreducible iff B ` is irreducible )
let B be Subset of T; ::_thesis: ( A = B & A <> Top (InclPoset the topology of T) implies ( A is irreducible iff B ` is irreducible ) )
assume that
A1: A = B and
A2: A <> Top (InclPoset the topology of T) ; ::_thesis: ( A is irreducible iff B ` is irreducible )
A3: the carrier of (InclPoset the topology of T) = the topology of T by YELLOW_1:1;
hereby  ::_thesis: ( B ` is irreducible implies A is irreducible )
assume A4: A is irreducible ; ::_thesis: B ` is irreducible
thus  B ` is irreducible ::_thesis: verum
proof
A5: B <> the carrier of T by A1, A2, YELLOW_1:24;
now__::_thesis:_not_the_carrier_of_T_\_B_=_{}
assume  the carrier of T \ B = {} ; ::_thesis: contradiction
then  the carrier of T c= B by XBOOLE_1:37;
hence  contradiction by A5, XBOOLE_0:def_10; ::_thesis: verum
end;
hence  not B ` is empty ; :: according to YELLOW_8:def_3 ::_thesis: ( B ` is closed & ( for b1, b2 being Element of bool the carrier of T holds
( not b1 is closed or not b2 is closed or not B ` = b1 \/ b2 or b1 = B ` or b2 = B ` ) ) )
 (B `) ` is open by A1, A3, PRE_TOPC:def_2;
hence  B ` is closed ; ::_thesis: for b1, b2 being Element of bool the carrier of T holds
( not b1 is closed or not b2 is closed or not B ` = b1 \/ b2 or b1 = B ` or b2 = B ` )
let S1, S2 be Subset of T; ::_thesis: ( not S1 is closed or not S2 is closed or not B ` = S1 \/ S2 or S1 = B ` or S2 = B ` )
assume that
A6: ( S1 is closed & S2 is closed ) and
A7: B ` = S1 \/ S2 ; ::_thesis: ( S1 = B ` or S2 = B ` )
A8: ( S1 ` is open & S2 ` is open ) by A6;
then reconsider s1 = S1 ` , s2 = S2 ` as Element of (InclPoset the topology of T) by A3, PRE_TOPC:def_2;
 (S1 `) /\ (S2 `) is open by A8;
then A9: s1 /\ s2 in the topology of T by PRE_TOPC:def_2;
B = (S1 \/ S2) ` by A7
.= (S1 `) /\ (S2 `) by XBOOLE_1:53 ;
then  A = s1 "/\" s2 by A1, A9, YELLOW_1:9;
then  ( A = s1 or A = s2 ) by A4, WAYBEL_6:def_2;
hence  ( S1 = B ` or S2 = B ` ) by A1; ::_thesis: verum
end;
end;
thus  ( B ` is irreducible implies A is irreducible ) by A1, Th40; ::_thesis: verum
end;

theorem Th42: :: WAYBEL12:42
for T being non empty TopSpace
for A being Element of (InclPoset the topology of T)
for B being Subset of T st A = B holds
( A is dense iff B is everywhere_dense )
proof
let T be non empty TopSpace; ::_thesis: for A being Element of (InclPoset the topology of T)
for B being Subset of T st A = B holds
( A is dense iff B is everywhere_dense )
let A be Element of (InclPoset the topology of T); ::_thesis: for B being Subset of T st A = B holds
( A is dense iff B is everywhere_dense )
let B be Subset of T; ::_thesis: ( A = B implies ( A is dense iff B is everywhere_dense ) )
assume A1: A = B ; ::_thesis: ( A is dense iff B is everywhere_dense )
A2: Bottom (InclPoset the topology of T) = {} by PRE_TOPC:1, YELLOW_1:13;
A3: the carrier of (InclPoset the topology of T) = the topology of T by YELLOW_1:1;
then A4: B is open by A1, PRE_TOPC:def_2;
hereby  ::_thesis: ( B is everywhere_dense implies A is dense )
assume A5: A is dense ; ::_thesis: B is everywhere_dense
 for Q being Subset of T st Q <> {} & Q is open holds
B meets Q
proof
let Q be Subset of T; ::_thesis: ( Q <> {} & Q is open implies B meets Q )
assume that
A6: Q <> {} and
A7: Q is open ; ::_thesis: B meets Q
reconsider q = Q as Element of (InclPoset the topology of T) by A3, A7, PRE_TOPC:def_2;
 B /\ Q is open by A4, A7;
then A8: A /\ q in the topology of T by A1, PRE_TOPC:def_2;
 A "/\" q <> Bottom (InclPoset the topology of T) by A2, A5, A6, Def4;
then  B /\ Q <> {} by A1, A2, A8, YELLOW_1:9;
hence  B meets Q by XBOOLE_0:def_7; ::_thesis: verum
end;
then  B is dense by TOPS_1:45;
hence  B is everywhere_dense by A4, TOPS_3:36; ::_thesis: verum
end;
assume  B is everywhere_dense ; ::_thesis: A is dense
then A9: B is dense by TOPS_3:33;
let v be Element of (InclPoset the topology of T); :: according to WAYBEL12:def_4 ::_thesis: ( v <> Bottom (InclPoset the topology of T) implies A "/\" v <> Bottom (InclPoset the topology of T) )
assume A10: v <> Bottom (InclPoset the topology of T) ; ::_thesis: A "/\" v <> Bottom (InclPoset the topology of T)
 v in the topology of T by A3;
then reconsider V = v as Subset of T ;
A11: V is open by A3, PRE_TOPC:def_2;
 B is open by A1, A3, PRE_TOPC:def_2;
then  B /\ V is open by A11;
then A12: B /\ V in the topology of T by PRE_TOPC:def_2;
 B meets V by A2, A9, A10, A11, TOPS_1:45;
then  B /\ V <> {} by XBOOLE_0:def_7;
hence  A "/\" v <> Bottom (InclPoset the topology of T) by A1, A2, A12, YELLOW_1:9; ::_thesis: verum
end;

theorem Th43: :: WAYBEL12:43
for T being non empty TopSpace st T is locally-compact holds
for D being countable Subset-Family of T st not D is empty & D is dense & D is open holds
for O being non empty Subset of T st O is open holds
ex A being irreducible Subset of T st
for V being Subset of T st V in D holds
A /\ O meets V
proof
let T be non empty TopSpace; ::_thesis: ( T is locally-compact implies for D being countable Subset-Family of T st not D is empty & D is dense & D is open holds
for O being non empty Subset of T st O is open holds
ex A being irreducible Subset of T st
for V being Subset of T st V in D holds
A /\ O meets V )
assume  T is locally-compact ; ::_thesis: for D being countable Subset-Family of T st not D is empty & D is dense & D is open holds
for O being non empty Subset of T st O is open holds
ex A being irreducible Subset of T st
for V being Subset of T st V in D holds
A /\ O meets V
then reconsider L = InclPoset the topology of T as bounded continuous LATTICE by WAYBEL_3:42;
A1: the carrier of L = the topology of T by YELLOW_1:1;
let D be countable Subset-Family of T; ::_thesis: ( not D is empty & D is dense & D is open implies for O being non empty Subset of T st O is open holds
ex A being irreducible Subset of T st
for V being Subset of T st V in D holds
A /\ O meets V )
assume A2: ( not D is empty & D is dense & D is open ) ; ::_thesis: for O being non empty Subset of T st O is open holds
ex A being irreducible Subset of T st
for V being Subset of T st V in D holds
A /\ O meets V
consider I being set  such that
A3: I in D by A2, XBOOLE_0:def_1;
reconsider I = I as Subset of T by A3;
 I is open by A2, A3, TOPS_2:def_1;
then reconsider i = I as Element of L by A1, PRE_TOPC:def_2;
set D1 =  {  d where d is Element of L : ex d1 being Subset of T st
( d1 in D & d1 = d & d is dense )  }  ;
  {  d where d is Element of L : ex d1 being Subset of T st
( d1 in D & d1 = d & d is dense )  }  c= the carrier of L
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in  {  d where d is Element of L : ex d1 being Subset of T st
( d1 in D & d1 = d & d is dense )  }  or q in the carrier of L )
assume  q in  {  d where d is Element of L : ex d1 being Subset of T st
( d1 in D & d1 = d & d is dense )  }  ; ::_thesis: q in the carrier of L
then  ex d being Element of L st
( q = d & ex d1 being Subset of T st
( d1 in D & d1 = d & d is dense ) ) ;
hence  q in the carrier of L ; ::_thesis: verum
end;
then reconsider D1 =  {  d where d is Element of L : ex d1 being Subset of T st
( d1 in D & d1 = d & d is dense )  }  as Subset of L ;
A4: D1 c= D
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in D1 or q in D )
assume  q in D1 ; ::_thesis: q in D
then  ex d being Element of L st
( q = d & ex d1 being Subset of T st
( d1 in D & d1 = d & d is dense ) ) ;
hence  q in D ; ::_thesis: verum
end;
A5: D1 is dense
proof
let q be Element of L; :: according to WAYBEL12:def_5 ::_thesis: ( q in D1 implies q is dense )
assume  q in D1 ; ::_thesis: q is dense
then  ex d being Element of L st
( q = d & ex d1 being Subset of T st
( d1 in D & d1 = d & d is dense ) ) ;
hence  q is dense ; ::_thesis: verum
end;
let O be non empty Subset of T; ::_thesis: ( O is open implies ex A being irreducible Subset of T st
for V being Subset of T st V in D holds
A /\ O meets V )
assume A6: O is open ; ::_thesis: ex A being irreducible Subset of T st
for V being Subset of T st V in D holds
A /\ O meets V
reconsider u = O as Element of L by A6, A1, PRE_TOPC:def_2;
 ( I is open & I is dense ) by A2, A3, Def2, TOPS_2:def_1;
then  I is everywhere_dense by TOPS_3:36;
then  i is dense by Th42;
then  ( u <> Bottom L & i in D1 ) by A3, PRE_TOPC:1, YELLOW_1:13;
then consider p being irreducible Element of L such that
A7: p <> Top L and
A8: not p in uparrow ({u} "/\" D1) by A4, A5, Th39;
 p in the topology of T by A1;
then reconsider P = p as Subset of T ;
reconsider A = P ` as irreducible Subset of T by A7, Th41;
take  A ; ::_thesis: for V being Subset of T st V in D holds
A /\ O meets V
let V be Subset of T; ::_thesis: ( V in D implies A /\ O meets V )
assume A9: V in D ; ::_thesis: A /\ O meets V
then A10: V is open by A2, TOPS_2:def_1;
then reconsider v = V as Element of L by A1, PRE_TOPC:def_2;
A11: for d1 being Element of L st d1 in D1 holds
not u "/\" d1 <= p
proof
A12: u in {u} by TARSKI:def_1;
let d1 be Element of L; ::_thesis: ( d1 in D1 implies not u "/\" d1 <= p )
assume  d1 in D1 ; ::_thesis: not u "/\" d1 <= p
then  u "/\" d1 in {u} "/\" D1 by A12;
hence  not u "/\" d1 <= p by A8, WAYBEL_0:def_16; ::_thesis: verum
end;
 V is dense by A2, A9, Def2;
then  V is everywhere_dense by A10, TOPS_3:36;
then  v is dense by Th42;
then  v in D1 by A9;
then  not u "/\" v <= p by A11;
then A13: not u "/\" v c= p by YELLOW_1:3;
 O /\ V is open by A6, A10;
then  u /\ v in the topology of T by PRE_TOPC:def_2;
then  not O /\ V c= p by A13, YELLOW_1:9;
then consider x being set  such that
A14: x in O /\ V and
A15: not x in A ` by TARSKI:def_3;
reconsider x = x as Element of T by A14;
 x in A by A15, XBOOLE_0:def_5;
then  (O /\ V) /\ A <> {} by A14, XBOOLE_0:def_4;
hence  (A /\ O) /\ V <> {} by XBOOLE_1:16; :: according to XBOOLE_0:def_7 ::_thesis: verum
end;

definition
let T be non empty TopSpace;
redefine attr T is Baire  means :: WAYBEL12:def 6
 for F being Subset-Family of T st F is countable & ( for S being Subset of T st S in F holds
( S is open & S is dense ) ) holds
ex I being Subset of T st
( I = Intersect F & I is dense );
compatibility
 ( T is Baire iff for F being Subset-Family of T st F is countable & ( for S being Subset of T st S in F holds
( S is open & S is dense ) ) holds
ex I being Subset of T st
( I = Intersect F & I is dense ) )
proof
set D = bool the carrier of T;
hereby  ::_thesis: ( ( for F being Subset-Family of T st F is countable & ( for S being Subset of T st S in F holds
( S is open & S is dense ) ) holds
ex I being Subset of T st
( I = Intersect F & I is dense ) ) implies T is Baire )
assume A1: T is Baire ; ::_thesis: for F being Subset-Family of T st F is countable & ( for S being Subset of T st S in F holds
( S is open & S is dense ) ) holds
ex I being Subset of T st
( I = Intersect F & I is dense )
thus  for F being Subset-Family of T st F is countable & ( for S being Subset of T st S in F holds
( S is open & S is dense ) ) holds
ex I being Subset of T st
( I = Intersect F & I is dense ) ::_thesis: verum
proof
let F be Subset-Family of T; ::_thesis: ( F is countable & ( for S being Subset of T st S in F holds
( S is open & S is dense ) ) implies ex I being Subset of T st
( I = Intersect F & I is dense ) )
assume that
A2: F is countable and
A3: for S being Subset of T st S in F holds
( S is open & S is dense ) ; ::_thesis: ex I being Subset of T st
( I = Intersect F & I is dense )
 for S being Subset of T st S in F holds
S is everywhere_dense
proof
let S be Subset of T; ::_thesis: ( S in F implies S is everywhere_dense )
assume  S in F ; ::_thesis: S is everywhere_dense
then  ( S is open & S is dense ) by A3;
hence  S is everywhere_dense by TOPS_3:36; ::_thesis: verum
end;
hence  ex I being Subset of T st
( I = Intersect F & I is dense ) by A1, A2, YELLOW_8:def_2; ::_thesis: verum
end;
end;
assume A4: for F being Subset-Family of T st F is countable & ( for S being Subset of T st S in F holds
( S is open & S is dense ) ) holds
ex I being Subset of T st
( I = Intersect F & I is dense ) ; ::_thesis: T is Baire
deffunc H1( Element of bool the carrier of T) ->  Element of bool the carrier of T = Int $1;
let F be Subset-Family of T; :: according to YELLOW_8:def_2 ::_thesis: ( not F is countable or ex b1 being Element of bool the carrier of T st
( b1 in F & not b1 is everywhere_dense ) or ex b1 being Element of bool the carrier of T st
( b1 = Intersect F & b1 is dense ) )
assume that
A5: F is countable and
A6: for S being Subset of T st S in F holds
S is everywhere_dense ; ::_thesis: ex b1 being Element of bool the carrier of T st
( b1 = Intersect F & b1 is dense )
set F1 =  {  (Int A) where A is Subset of T : A in F  }  ;
consider f being Function of (bool the carrier of T),(bool the carrier of T) such that
A7: for x being Element of bool the carrier of T holds f . x = H1(x) from FUNCT_2:sch_4();
  {  (Int A) where A is Subset of T : A in F  }  c= f .: F
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in  {  (Int A) where A is Subset of T : A in F  }  or q in f .: F )
assume  q in  {  (Int A) where A is Subset of T : A in F  }  ; ::_thesis: q in f .: F
then consider A being Subset of T such that
A8: ( q = Int A & A in F ) ;
 ( dom f = bool the carrier of T & f . A = Int A ) by A7, FUNCT_2:def_1;
hence  q in f .: F by A8, FUNCT_1:def_6; ::_thesis: verum
end;
then  card  {  (Int A) where A is Subset of T : A in F  }  c= card F by CARD_1:66;
then A9:  {  (Int A) where A is Subset of T : A in F  }  is countable by A5, Th1;
reconsider J = Intersect F as Subset of T ;
A10:  {  (Int A) where A is Subset of T : A in F  }  c= bool the carrier of T
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in  {  (Int A) where A is Subset of T : A in F  }  or q in bool the carrier of T )
assume  q in  {  (Int A) where A is Subset of T : A in F  }  ; ::_thesis: q in bool the carrier of T
then  ex A being Subset of T st
( q = Int A & A in F ) ;
hence  q in bool the carrier of T ; ::_thesis: verum
end;
take  J ; ::_thesis: ( J = Intersect F & J is dense )
thus  J = Intersect F ; ::_thesis: J is dense
reconsider F1 =  {  (Int A) where A is Subset of T : A in F  }  as Subset-Family of T by A10;
 for X being set st X in F holds
Intersect F1 c= X
proof
let X be set ; ::_thesis: ( X in F implies Intersect F1 c= X )
assume A11: X in F ; ::_thesis: Intersect F1 c= X
reconsider X1 = X as Subset of T by A11;
A12: Int X1 in F1 by A11;
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in Intersect F1 or q in X )
assume  q in Intersect F1 ; ::_thesis: q in X
then  ( Int X1 c= X1 & q in Int X1 ) by A12, SETFAM_1:43, TOPS_1:16;
hence  q in X ; ::_thesis: verum
end;
then A13: Intersect F1 c= Intersect F by MSSUBFAM:4;
now__::_thesis:_for_S_being_Subset_of_T_st_S_in_F1_holds_
(_S_is_open_&_S_is_dense_)
let S be Subset of T; ::_thesis: ( S in F1 implies ( S is open & S is dense ) )
assume  S in F1 ; ::_thesis: ( S is open & S is dense )
then consider A being Subset of T such that
A14: S = Int A and
A15: A in F ;
 A is everywhere_dense by A6, A15;
hence  ( S is open & S is dense ) by A14, TOPS_3:35; ::_thesis: verum
end;
then  ex I being Subset of T st
( I = Intersect F1 & I is dense ) by A4, A9;
hence  J is dense by A13, TOPS_1:44; ::_thesis: verum
end;
end;

:: deftheorem  defines Baire WAYBEL12:def_6_:_
 for T being non empty TopSpace holds
( T is Baire iff for F being Subset-Family of T st F is countable & ( for S being Subset of T st S in F holds
( S is open & S is dense ) ) holds
ex I being Subset of T st
( I = Intersect F & I is dense ) );

theorem :: WAYBEL12:44
for T being non empty TopSpace st T is sober & T is locally-compact holds
T is Baire
proof
let T be non empty TopSpace; ::_thesis: ( T is sober & T is locally-compact implies T is Baire )
assume A1: ( T is sober & T is locally-compact ) ; ::_thesis: T is Baire
let F be Subset-Family of T; :: according to WAYBEL12:def_6 ::_thesis: ( F is countable & ( for S being Subset of T st S in F holds
( S is open & S is dense ) ) implies ex I being Subset of T st
( I = Intersect F & I is dense ) )
assume that
A2: F is countable and
A3: for S being Subset of T st S in F holds
( S is open & S is dense ) ; ::_thesis: ex I being Subset of T st
( I = Intersect F & I is dense )
A4: F is open
proof
let X be Subset of T; :: according to TOPS_2:def_1 ::_thesis: ( not X in F or X is open )
assume  X in F ; ::_thesis: X is open
hence  X is open by A3; ::_thesis: verum
end;
 for X being Subset of T st X in F holds
X is dense by A3;
then A5: ( F is open & F is dense ) by A4, Def2;
reconsider I = Intersect F as Subset of T ;
take  I ; ::_thesis: ( I = Intersect F & I is dense )
thus  I = Intersect F ; ::_thesis: I is dense
percases ( F <> {} or F = {} ) ;
supposeA6: F <> {} ; ::_thesis: I is dense
 for Q being Subset of T st Q <> {} & Q is open holds
Intersect F meets Q
proof
let Q be Subset of T; ::_thesis: ( Q <> {} & Q is open implies Intersect F meets Q )
assume that
A7: Q <> {} and
A8: Q is open ; ::_thesis: Intersect F meets Q
consider S being irreducible Subset of T such that
A9: for V being Subset of T st V in F holds
S /\ Q meets V by A1, A2, A5, A6, A7, A8, Th43;
consider p being Point of T such that
A10: p is_dense_point_of S and
 for q being Point of T st q is_dense_point_of S holds
p = q by A1, YELLOW_8:def_5;
 S is closed by YELLOW_8:def_3;
then A11: S = Cl {p} by A10, YELLOW_8:16;
A12: for Y being set st Y in F holds
( p in Y & p in Q )
proof
let Y be set ; ::_thesis: ( Y in F implies ( p in Y & p in Q ) )
assume A13: Y in F ; ::_thesis: ( p in Y & p in Q )
then reconsider Y1 = Y as Subset of T ;
 S /\ Q meets Y1 by A9, A13;
then A14: (S /\ Q) /\ Y1 <> {} by XBOOLE_0:def_7;
now__::_thesis:_p_in_Q_/\_Y1
assume  not p in Q /\ Y1 ; ::_thesis: contradiction
then  p in (Q /\ Y1) ` by XBOOLE_0:def_5;
then  {p} c= (Q /\ Y1) ` by ZFMISC_1:31;
then A15: Cl {p} c= Cl ((Q /\ Y1) `) by PRE_TOPC:19;
 Y1 is open by A3, A13;
then  Q /\ Y1 is open by A8;
then  (Q /\ Y1) ` is closed ;
then  S c= (Q /\ Y1) ` by A11, A15, PRE_TOPC:22;
then  S misses Q /\ Y1 by SUBSET_1:23;
then  S /\ (Q /\ Y1) = {} by XBOOLE_0:def_7;
hence  contradiction by A14, XBOOLE_1:16; ::_thesis: verum
end;
hence  ( p in Y & p in Q ) by XBOOLE_0:def_4; ::_thesis: verum
end;
then  for Y being set st Y in F holds
p in Y ;
then A16: p in Intersect F by SETFAM_1:43;
 ex Y being set st Y in F by A6, XBOOLE_0:def_1;
then  p in Q by A12;
then  (Intersect F) /\ Q <> {} by A16, XBOOLE_0:def_4;
hence  Intersect F meets Q by XBOOLE_0:def_7; ::_thesis: verum
end;
hence  I is dense by TOPS_1:45; ::_thesis: verum
end;
suppose F = {} ; ::_thesis: I is dense
then  Intersect F = [#] T by SETFAM_1:def_9;
hence  I is dense ; ::_thesis: verum
end;
end;
end;