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 set ; :: 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 & 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 & ex_inf_of X,R ) by WAYBEL_0:76;
then A6: inf X >= inf F by A3, 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
A7: ( b in F & a >= b & j >= b ) by A2, WAYBEL_0:def 2;
reconsider k = b as Element of (F opp+id ) by A7, YELLOW_9:7;
( F opp+id is full SubRelStr of R opp & j ~ = v & b ~ = k & j ~ <= b ~ ) by A7, LATTICE3:9, YELLOW_9:7;
then ( (F opp+id ) . k = b & k >= vv ) by YELLOW_0:61, YELLOW_9:7;
then b in X ;
then ( {b} c= X & ex_inf_of {b},R & inf {b} = b ) by YELLOW_0:38, YELLOW_0:39, ZFMISC_1:37;
then b >= inf X by A5, YELLOW_0:35;
hence inf X <= a by A7, 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 A6, ORDERS_2:25; :: thesis: verum

end;

A8: { 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);
A9: 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(A9);
hence lim_inf (F opp+id ) = "\/" {(inf F)},R by A8, WAYBEL11:def 6
.= inf F by YELLOW_0:39 ;
:: thesis: verum