let L be TopLattice; :: thesis: for x being Element of L st ( for X being Subset of L st X is open holds
X is upper ) holds
uparrow x is compact
let x be Element of L; :: thesis: ( ( for X being Subset of L st X is open holds
X is upper ) implies uparrow x is compact )
assume A1: for X being Subset of L st X is open holds
X is upper ; :: thesis: uparrow x is compact
set P = uparrow x;
let F be Subset-Family of L; :: according to COMPTS_1:def 4 :: thesis: ( not F is Cover of uparrow x or not F is open or ex b₁ being Element of bool (bool the carrier of L) st
( b₁ c= F & b₁ is Cover of uparrow x & b₁ is finite ) )
assume that
A2: F is Cover of uparrow x and
A3: F is open ; :: thesis: ex b₁ being Element of bool (bool the carrier of L) st
( b₁ c= F & b₁ is Cover of uparrow x & b₁ is finite )
x <= x ;
then A4: x in uparrow x by WAYBEL_0:18;
uparrow x c= union F by A2, SETFAM_1:def 11;
then consider Y being set such that
A5: x in Y and
A6: Y in F by A4, TARSKI:def 4;
reconsider Y = Y as Subset of L by A6;
reconsider G = {Y} as Subset-Family of L ;
reconsider G = G as Subset-Family of L ;
take G ; :: thesis: ( G c= F & G is Cover of uparrow x & G is finite )
thus G c= F by A6, ZFMISC_1:31; :: thesis: ( G is Cover of uparrow x & G is finite )
Y is open by A3, A6;
then Y is upper by A1;
then uparrow x c= Y by A5, WAYBEL11:42;
hence uparrow x c= union G by ZFMISC_1:25; :: according to SETFAM_1:def 11 :: thesis: G is finite
thus G is finite ; :: thesis: verum