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)}_{1}[ Element of (f * (Net-Str (a,b))), Element of (f * (Net-Str (a,b)))] means $1 >= $2;

deffunc H_{1}( 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_{1}[i1,$1] } ;

defpred S_{2}[ set ] means verum;

deffunc H_{2}( Element of (f * (Net-Str (a,b)))) -> Element of K32( the carrier of T) = {(f . a),(f . b)};

deffunc H_{3}( Element of (f * (Net-Str (a,b)))) -> Element of the carrier of T = "/\" (H_{1}($1),T);

deffunc H_{4}( Element of (f * (Net-Str (a,b)))) -> Element of the carrier of T = "/\" (H_{2}($1),T);

deffunc H_{5}( set ) -> Element of the carrier of T = (f . a) "/\" (f . b);

A22: for jj being Element of (f * (Net-Str (a,b))) holds H_{3}(jj) = H_{5}(jj)
_{3}(j3) where j3 is Element of (f * (Net-Str (a,b))) : S_{2}[j3] } = { H_{5}(j4) where j4 is Element of (f * (Net-Str (a,b))) : S_{2}[j4] }
from FRAENKEL:sch 5(A22);

A24: { ((f . a) "/\" (f . b)) where j4 is Element of (f * (Net-Str (a,b))) : S_{2}[j4] } c= {((f . a) "/\" (f . b))}
_{2}[j4] }
_{2}[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

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

defpred S
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 }

end;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

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
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;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

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_{1}[ Element of NAT ] means ex k being Element of NAT st $1 = 2 * k;

end;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

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

end;

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;

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

hence
x in { ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j }
; :: thesis: verumper cases
( S_{1}[J] or not S_{1}[J] )
;

end;

suppose A9:
S_{1}[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;.= 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

suppose A11:
not S_{1}[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;.= 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

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 }

end;

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

hence
x in { ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j }
; :: thesis: verumper cases
( not S_{1}[J] or S_{1}[J] )
;

end;

suppose A16:
not S_{1}[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;.= 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

suppose A18:
S_{1}[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;.= 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

deffunc H

defpred S

deffunc H

deffunc H

deffunc H

deffunc H

A22: for jj being Element of (f * (Net-Str (a,b))) holds H

proof

A23:
{ H
let jj be Element of (f * (Net-Str (a,b))); :: thesis: H_{3}(jj) = H_{5}(jj)

H_{3}(jj) =
H_{4}(jj)
by A2

.= (f . a) "/\" (f . b) by YELLOW_0:40 ;

hence H_{3}(jj) = H_{5}(jj)
; :: thesis: verum

end;H

.= (f . a) "/\" (f . b) by YELLOW_0:40 ;

hence H

A24: { ((f . a) "/\" (f . b)) where j4 is Element of (f * (Net-Str (a,b))) : S

proof

{((f . a) "/\" (f . b))} c= { ((f . a) "/\" (f . b)) where j4 is Element of (f * (Net-Str (a,b))) : S
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_{2}[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_{2}[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_{2}[q] )
;

hence x in {((f . a) "/\" (f . b))} by TARSKI:def 1; :: thesis: verum

end;assume x in { ((f . a) "/\" (f . b)) where j4 is Element of (f * (Net-Str (a,b))) : S

then ex q being Element of (f * (Net-Str (a,b))) st

( x = (f . a) "/\" (f . b) & S

hence x in {((f . a) "/\" (f . b))} by TARSKI:def 1; :: thesis: verum

proof

then
{ ((f . a) "/\" (f . b)) where j4 is Element of (f * (Net-Str (a,b))) : S
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_{2}[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_{2}[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_{2}[j4] }
; :: thesis: verum

end;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

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

hence lim_inf (f * (Net-Str (a,b))) = (f . a) "/\" (f . b) by A23, YELLOW_0:39; :: thesis: verum