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 object ; :: 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:13 ;
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 object ; :: 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 :: thesis: x in { ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j }

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:13
.= 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:13
.= 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 5;
then k >= j by A1, ORDERS_2:def 5;
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 :: thesis: x in { ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j }

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:13
.= 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:13
.= 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 5;
then k >= j by A1, ORDERS_2:def 5;
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 K32( 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 object ; :: 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 object ; :: 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;
hence lim_inf (f * (Net-Str (a,b))) = (f . a) "/\" (f . b) by A23, YELLOW_0:39; :: thesis: verum