let T be complete lower TopLattice; :: thesis: for BB being prebasis of T
for F being non empty filtered Subset of T st ( for A being Subset of T st A in BB & inf F in A holds
F meets A ) holds
inf F in Cl F
let BB be prebasis of T; :: thesis: for F being non empty filtered Subset of T st ( for A being Subset of T st A in BB & inf F in A holds
F meets A ) holds
inf F in Cl F
let F be non empty filtered Subset of T; :: thesis: ( ( for A being Subset of T st A in BB & inf F in A holds
F meets A ) implies inf F in Cl F )
assume A1: for A being Subset of T st A in BB & inf F in A holds
F meets A ; :: thesis: inf F in Cl F
set N = F opp+id ;
set x = inf F;
A2: the carrier of (F opp+id ) = F by YELLOW_9:7;
A3: for A being Subset of T st A in BB & inf F in A holds
F opp+id is_eventually_in A

proof

let A be Subset of T; :: thesis: ( A in BB & inf F in A implies F opp+id is_eventually_in A )
assume A4: ( A in BB & inf F in A ) ; :: thesis: F opp+id is_eventually_in A
then F meets A by A1;
then consider i being set such that
A5: ( i in F & i in A ) by XBOOLE_0:3;
reconsider i = i as Element of (F opp+id ) by A5, YELLOW_9:7;
take i ; :: according to WAYBEL_0:def 11 :: thesis: for b₁ being Element of the carrier of (F opp+id ) holds
( not i <= b₁ or (F opp+id ) . b₁ in A )
BB is open by YELLOW_9:28;
then A is open by A4, TOPS_2:def 1;
then A6: A is lower by Th5;
let j be Element of (F opp+id ); :: thesis: ( not i <= j or (F opp+id ) . j in A )
A7: ( (F opp+id ) . i = i & (F opp+id ) . j = j ) by YELLOW_9:7;
A8: F opp+id is full SubRelStr of T opp by YELLOW_9:7;
then reconsider a = i, b = j as Element of (T opp ) by YELLOW_0:59;
assume i <= j ; :: thesis: (F opp+id ) . j in A
then a <= b by A8, YELLOW_0:60;
then ~ b <= ~ a by YELLOW_7:1;
hence (F opp+id ) . j in A by A5, A6, A7, WAYBEL_0:def 19; :: thesis: verum

end;

rng (netmap (F opp+id ),T) c= F

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (netmap (F opp+id ),T) or x in F )
assume x in rng (netmap (F opp+id ),T) ; :: thesis: x in F
then consider a being set such that
A9: ( a in dom (netmap (F opp+id ),T) & x = (netmap (F opp+id ),T) . a ) by FUNCT_1:def 5;
reconsider a = a as Element of (F opp+id ) by A9;
x = (F opp+id ) . a by A9
.= a by YELLOW_9:7 ;
hence x in F by A2; :: thesis: verum

end;

hence inf F in Cl F by A3, YELLOW_9:39; :: thesis: verum