let S, T be with_infima Poset; :: thesis: for a, b being Element of S
for f being Function of S,T holds lim_inf (f * (Net-Str a,b)) = (f . a) "/\" (f . b)
let a, b be Element of S; :: thesis: for f being Function of S,T holds lim_inf (f * (Net-Str a,b)) = (f . a) "/\" (f . b)
let f be Function of S,T; :: thesis: lim_inf (f * (Net-Str a,b)) = (f . a) "/\" (f . b)
set N = Net-Str a,b;
set fN = f * (Net-Str a,b);
A1: RelStr(# the carrier of (f * (Net-Str a,b)),the InternalRel of (f * (Net-Str a,b)) #) = RelStr(# the carrier of (Net-Str a,b),the InternalRel of (Net-Str a,b) #) by WAYBEL_9:def 8;
A2: for j being Element of (f * (Net-Str a,b)) holds { ((f * (Net-Str a,b)) . i) where i is Element of (f * (Net-Str a,b)) : i >= j } = {(f . a),(f . b)}

proof

let j be Element of (f * (Net-Str a,b)); :: thesis: { ((f * (Net-Str a,b)) . i) where i is Element of (f * (Net-Str a,b)) : i >= j } = {(f . a),(f . b)}
reconsider jj = j as Element of (Net-Str a,b) by A1;
thus { ((f * (Net-Str a,b)) . i) where i is Element of (f * (Net-Str a,b)) : i >= j } c= {(f . a),(f . b)} :: according to XBOOLE_0:def 10 :: thesis: {(f . a),(f . b)} c= { ((f * (Net-Str a,b)) . i) where i is Element of (f * (Net-Str a,b)) : i >= j }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { ((f * (Net-Str a,b)) . i) where i is Element of (f * (Net-Str a,b)) : i >= j } or x in {(f . a),(f . b)} )
assume x in { ((f * (Net-Str a,b)) . i) where i is Element of (f * (Net-Str a,b)) : i >= j } ; :: thesis: x in {(f . a),(f . b)}
then consider i1 being Element of (f * (Net-Str a,b)) such that
A3: x = (f * (Net-Str a,b)) . i1 and
i1 >= j ;
reconsider I1 = i1 as Element of (Net-Str a,b) by A1;
i1 in the carrier of (Net-Str a,b) by A1;
then A4: i1 in dom the mapping of (Net-Str a,b) by FUNCT_2:def 1;
(f * (Net-Str a,b)) . i1 = (f * the mapping of (Net-Str a,b)) . i1 by WAYBEL_9:def 8
.= f . ((Net-Str a,b) . I1) by A4, FUNCT_1:23 ;
then ( (f * (Net-Str a,b)) . i1 = f . a or (f * (Net-Str a,b)) . i1 = f . b ) by Th5;
hence x in {(f . a),(f . b)} by A3, TARSKI:def 2; :: thesis: verum

end;

thus {(f . a),(f . b)} c= { ((f * (Net-Str a,b)) . i) where i is Element of (f * (Net-Str a,b)) : i >= j } :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {(f . a),(f . b)} or x in { ((f * (Net-Str a,b)) . i) where i is Element of (f * (Net-Str a,b)) : i >= j } )
assume A5: x in {(f . a),(f . b)} ; :: thesis: x in { ((f * (Net-Str a,b)) . i) where i is Element of (f * (Net-Str a,b)) : i >= j }
A6: j in the carrier of (Net-Str a,b) by A1;
reconsider J = j as Element of NAT by A1, Def3;
A7: j in dom the mapping of (Net-Str a,b) by A6, FUNCT_2:def 1;
defpred S₁[ Element of NAT ] means ex k being Element of NAT st $1 = 2 * k;

per cases ( x = f . a or x = f . b ) by A5, TARSKI:def 2;

suppose A8: x = f . a ; :: thesis: x in { ((f * (Net-Str a,b)) . i) where i is Element of (f * (Net-Str a,b)) : i >= j }

reconsider jj = j as Element of (Net-Str a,b) by A1;

now

per cases ( S₁[J] or not S₁[J] ) ;

suppose A9: S₁[J] ; :: thesis: x in { ((f * (Net-Str a,b)) . i) where i is Element of (f * (Net-Str a,b)) : i >= j }

A10: (f * (Net-Str a,b)) . j = (f * the mapping of (Net-Str a,b)) . j by WAYBEL_9:def 8
.= f . (the mapping of (Net-Str a,b) . j) by A7, FUNCT_1:23
.= f . ((a,b ,... ) . j) by Def3
.= f . a by A9, Def1 ;
j <= j ;
hence x in { ((f * (Net-Str a,b)) . i) where i is Element of (f * (Net-Str a,b)) : i >= j } by A8, A10; :: thesis: verum

end;

suppose A11: not S₁[J] ; :: thesis: x in { ((f * (Net-Str a,b)) . i) where i is Element of (f * (Net-Str a,b)) : i >= j }

A12: (Net-Str a,b) . jj = (a,b ,... ) . jj by Def3
.= b by A11, Def1 ;
reconsider k = J + 1 as Element of (f * (Net-Str a,b)) by A1, Def3;
reconsider kk = k as Element of (Net-Str a,b) by A1;
kk in the carrier of (Net-Str a,b) ;
then A13: kk in dom the mapping of (Net-Str a,b) by FUNCT_2:def 1;
A14: (f * (Net-Str a,b)) . k = (f * the mapping of (Net-Str a,b)) . k by WAYBEL_9:def 8
.= f . ((Net-Str a,b) . kk) by A13, FUNCT_1:23
.= f . a by A12, Th6 ;
J + 1 >= J by NAT_1:11;
then kk >= jj by Def3;
then [jj,kk] in the InternalRel of (Net-Str a,b) by ORDERS_2:def 9;
then k >= j by A1, ORDERS_2:def 9;
hence x in { ((f * (Net-Str a,b)) . i) where i is Element of (f * (Net-Str a,b)) : i >= j } by A8, A14; :: thesis: verum

end;

end;

end;

hence x in { ((f * (Net-Str a,b)) . i) where i is Element of (f * (Net-Str a,b)) : i >= j } ; :: thesis: verum

end;

suppose A15: x = f . b ; :: thesis: x in { ((f * (Net-Str a,b)) . i) where i is Element of (f * (Net-Str a,b)) : i >= j }

now

per cases ( not S₁[J] or S₁[J] ) ;

suppose A16: not S₁[J] ; :: thesis: x in { ((f * (Net-Str a,b)) . i) where i is Element of (f * (Net-Str a,b)) : i >= j }

A17: (f * (Net-Str a,b)) . j = (f * the mapping of (Net-Str a,b)) . j by WAYBEL_9:def 8
.= f . (the mapping of (Net-Str a,b) . j) by A7, FUNCT_1:23
.= f . ((a,b ,... ) . j) by Def3
.= f . b by A16, Def1 ;
j <= j ;
hence x in { ((f * (Net-Str a,b)) . i) where i is Element of (f * (Net-Str a,b)) : i >= j } by A15, A17; :: thesis: verum

end;

suppose A18: S₁[J] ; :: thesis: x in { ((f * (Net-Str a,b)) . i) where i is Element of (f * (Net-Str a,b)) : i >= j }

A19: (Net-Str a,b) . jj = (a,b ,... ) . j by Def3
.= a by A18, Def1 ;
reconsider k = J + 1 as Element of (f * (Net-Str a,b)) by A1, Def3;
reconsider kk = k as Element of (Net-Str a,b) by Def3;
kk in the carrier of (Net-Str a,b) ;
then A20: kk in dom the mapping of (Net-Str a,b) by FUNCT_2:def 1;
A21: (f * (Net-Str a,b)) . k = (f * the mapping of (Net-Str a,b)) . k by WAYBEL_9:def 8
.= f . ((Net-Str a,b) . kk) by A20, FUNCT_1:23
.= f . b by A19, Th6 ;
J + 1 >= J by NAT_1:11;
then kk >= jj by Def3;
then [jj,kk] in the InternalRel of (Net-Str a,b) by ORDERS_2:def 9;
then k >= j by A1, ORDERS_2:def 9;
hence x in { ((f * (Net-Str a,b)) . i) where i is Element of (f * (Net-Str a,b)) : i >= j } by A15, A21; :: thesis: verum

end;

end;

end;

hence x in { ((f * (Net-Str a,b)) . i) where i is Element of (f * (Net-Str a,b)) : i >= j } ; :: thesis: verum

end;

end;

end;

end;

defpred S₁[ Element of (f * (Net-Str a,b)), Element of (f * (Net-Str a,b))] means $1 >= $2;
deffunc H₁( Element of (f * (Net-Str a,b))) -> set = { ((f * (Net-Str a,b)) . i1) where i1 is Element of (f * (Net-Str a,b)) : S₁[i1,$1] } ;
defpred S₂[ set ] means verum;
deffunc H₂( Element of (f * (Net-Str a,b))) -> Element of bool the carrier of T = {(f . a),(f . b)};
deffunc H₃( Element of (f * (Net-Str a,b))) -> Element of the carrier of T = "/\" H₁($1),T;
deffunc H₄( Element of (f * (Net-Str a,b))) -> Element of the carrier of T = "/\" H₂($1),T;
deffunc H₅( set ) -> Element of the carrier of T = (f . a) "/\" (f . b);
A22: for jj being Element of (f * (Net-Str a,b)) holds H₃(jj) = H₅(jj)

proof

let jj be Element of (f * (Net-Str a,b)); :: thesis: H₃(jj) = H₅(jj)
H₃(jj) = H₄(jj) by A2
.= (f . a) "/\" (f . b) by YELLOW_0:40 ;
hence H₃(jj) = H₅(jj) ; :: thesis: verum

end;

A23: { H₃(j3) where j3 is Element of (f * (Net-Str a,b)) : S₂[j3] } = { H₅(j4) where j4 is Element of (f * (Net-Str a,b)) : S₂[j4] } from FRAENKEL:sch 5(A22);
A24: { ((f . a) "/\" (f . b)) where j4 is Element of (f * (Net-Str a,b)) : S₂[j4] } c= {((f . a) "/\" (f . b))}

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { ((f . a) "/\" (f . b)) where j4 is Element of (f * (Net-Str a,b)) : S₂[j4] } or x in {((f . a) "/\" (f . b))} )
assume x in { ((f . a) "/\" (f . b)) where j4 is Element of (f * (Net-Str a,b)) : S₂[j4] } ; :: thesis: x in {((f . a) "/\" (f . b))}
then ex q being Element of (f * (Net-Str a,b)) st
( x = (f . a) "/\" (f . b) & S₂[q] ) ;
hence x in {((f . a) "/\" (f . b))} by TARSKI:def 1; :: thesis: verum

end;

{((f . a) "/\" (f . b))} c= { ((f . a) "/\" (f . b)) where j4 is Element of (f * (Net-Str a,b)) : S₂[j4] }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {((f . a) "/\" (f . b))} or x in { ((f . a) "/\" (f . b)) where j4 is Element of (f * (Net-Str a,b)) : S₂[j4] } )
assume x in {((f . a) "/\" (f . b))} ; :: thesis: x in { ((f . a) "/\" (f . b)) where j4 is Element of (f * (Net-Str a,b)) : S₂[j4] }
then x = (f . a) "/\" (f . b) by TARSKI:def 1;
hence x in { ((f . a) "/\" (f . b)) where j4 is Element of (f * (Net-Str a,b)) : S₂[j4] } ; :: thesis: verum

end;

then { ((f . a) "/\" (f . b)) where j4 is Element of (f * (Net-Str a,b)) : S₂[j4] } = {((f . a) "/\" (f . b))} by A24, XBOOLE_0:def 10;
hence lim_inf (f * (Net-Str a,b)) = (f . a) "/\" (f . b) by A23, YELLOW_0:39; :: thesis: verum