let R be non empty /\-complete Poset; :: thesis: for F being non empty filtered Subset of R holds lim_inf (F opp+id) = inf F
let F be non empty filtered Subset of R; :: thesis: lim_inf (F opp+id) = inf F
set N = F opp+id ;
defpred S₁[ set ] means verum;
deffunc H₁( Element of (F opp+id)) -> Element of the carrier of R = inf F;
deffunc H₂( Element of (F opp+id)) -> Element of the carrier of R = "/\" ( { ((F opp+id) . i) where i is Element of (F opp+id) : i >= $1 } ,R);
A1: for v being Element of (F opp+id) st S₁[v] holds
H₁(v) = H₂(v)

proof

let v be Element of (F opp+id); :: thesis: ( S₁[v] implies H₁(v) = H₂(v) )
set X = { ((F opp+id) . i) where i is Element of (F opp+id) : i >= v } ;
A2: the carrier of (F opp+id) = F by YELLOW_9:7;
then v in F ;
then reconsider j = v as Element of R ;
reconsider vv = v as Element of (F opp+id) ;
A3: { ((F opp+id) . i) where i is Element of (F opp+id) : i >= v } c= F

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { ((F opp+id) . i) where i is Element of (F opp+id) : i >= v } or x in F )
assume x in { ((F opp+id) . i) where i is Element of (F opp+id) : i >= v } ; :: thesis: x in F
then consider i being Element of (F opp+id) such that
A4: x = (F opp+id) . i and
i >= v ;
reconsider i = i as Element of (F opp+id) ;
x = i by A4, YELLOW_9:7;
hence x in F by A2; :: thesis: verum

end;

vv <= vv ;
then (F opp+id) . v in { ((F opp+id) . i) where i is Element of (F opp+id) : i >= v } ;
then reconsider X = { ((F opp+id) . i) where i is Element of (F opp+id) : i >= v } as non empty Subset of R by A3, XBOOLE_1:1;
A5: ex_inf_of F,R by WAYBEL_0:76;
A6: ex_inf_of X,R by WAYBEL_0:76;
then A7: inf X >= inf F by A3, A5, YELLOW_0:35;
F is_>=_than inf X

proof

let a be Element of R; :: according to LATTICE3:def 8 :: thesis: ( not a in F or inf X <= a )
assume a in F ; :: thesis: inf X <= a
then consider b being Element of R such that
A8: b in F and
A9: a >= b and
A10: j >= b by A2, WAYBEL_0:def 2;
reconsider k = b as Element of (F opp+id) by A8, YELLOW_9:7;
A11: F opp+id is full SubRelStr of R opp by YELLOW_9:7;
A12: j ~ <= b ~ by A10, LATTICE3:9;
A13: (F opp+id) . k = b by YELLOW_9:7;
k >= vv by A11, A12, YELLOW_0:60;
then b in X by A13;
then A14: {b} c= X by ZFMISC_1:31;
A15: ex_inf_of {b},R by YELLOW_0:38;
inf {b} = b by YELLOW_0:39;
then b >= inf X by A6, A14, A15, YELLOW_0:35;
hence inf X <= a by A9, YELLOW_0:def 2; :: thesis: verum

end;

then inf F >= "/\" (X,R) by A5, YELLOW_0:31;
hence ( S₁[v] implies H₁(v) = H₂(v) ) by A7, ORDERS_2:2; :: thesis: verum

end;

A16: { H₁(j) where j is Element of (F opp+id) : S₁[j] } = { H₂(k) where k is Element of (F opp+id) : S₁[k] } from FRAENKEL:sch 6(A1);
A17: ex j being Element of (F opp+id) st S₁[j] ;
{ (inf F) where j is Element of (F opp+id) : S₁[j] } = {(inf F)} from LATTICE3:sch 1(A17);
hence lim_inf (F opp+id) = "\/" ({(inf F)},R) by A16, WAYBEL11:def 6
.= inf F by YELLOW_0:39 ;
:: thesis: verum