let S be with_infima Poset; :: thesis: for a, b being Element of S holds lim_inf (Net-Str (a,b)) = a "/\" b

let a, b be Element of S; :: thesis: lim_inf (Net-Str (a,b)) = a "/\" b

set N = Net-Str (a,b);

A1: for j being Element of (Net-Str (a,b)) holds { ((Net-Str (a,b)) . i) where i is Element of (Net-Str (a,b)) : i >= j } = {a,b}_{1}[ Element of (Net-Str (a,b)), Element of (Net-Str (a,b))] means $1 >= $2;

deffunc H_{1}( Element of (Net-Str (a,b))) -> set = { ((Net-Str (a,b)) . i1) where i1 is Element of (Net-Str (a,b)) : S_{1}[i1,$1] } ;

defpred S_{2}[ set ] means verum;

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

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

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

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

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

A18: { (a "/\" b) where j4 is Element of (Net-Str (a,b)) : S_{2}[j4] } c= {(a "/\" b)}
_{2}[j4] }
_{2}[j4] } = {(a "/\" b)}
by A18;

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

let a, b be Element of S; :: thesis: lim_inf (Net-Str (a,b)) = a "/\" b

set N = Net-Str (a,b);

A1: for j being Element of (Net-Str (a,b)) holds { ((Net-Str (a,b)) . i) where i is Element of (Net-Str (a,b)) : i >= j } = {a,b}

proof

defpred S
let j be Element of (Net-Str (a,b)); :: thesis: { ((Net-Str (a,b)) . i) where i is Element of (Net-Str (a,b)) : i >= j } = {a,b}

thus { ((Net-Str (a,b)) . i) where i is Element of (Net-Str (a,b)) : i >= j } c= {a,b} :: according to XBOOLE_0:def 10 :: thesis: {a,b} c= { ((Net-Str (a,b)) . i) where i is Element of (Net-Str (a,b)) : i >= j }

end;thus { ((Net-Str (a,b)) . i) where i is Element of (Net-Str (a,b)) : i >= j } c= {a,b} :: according to XBOOLE_0:def 10 :: thesis: {a,b} c= { ((Net-Str (a,b)) . i) where i is Element of (Net-Str (a,b)) : i >= j }

proof

thus
{a,b} c= { ((Net-Str (a,b)) . i) where i is Element of (Net-Str (a,b)) : i >= j }
:: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { ((Net-Str (a,b)) . i) where i is Element of (Net-Str (a,b)) : i >= j } or x in {a,b} )

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

then consider i1 being Element of (Net-Str (a,b)) such that

A2: x = (Net-Str (a,b)) . i1 and

i1 >= j ;

( (Net-Str (a,b)) . i1 = a or (Net-Str (a,b)) . i1 = b ) by Th5;

hence x in {a,b} by A2, TARSKI:def 2; :: thesis: verum

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

then consider i1 being Element of (Net-Str (a,b)) such that

A2: x = (Net-Str (a,b)) . i1 and

i1 >= j ;

( (Net-Str (a,b)) . i1 = a or (Net-Str (a,b)) . i1 = b ) by Th5;

hence x in {a,b} by A2, TARSKI:def 2; :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {a,b} or x in { ((Net-Str (a,b)) . i) where i is Element of (Net-Str (a,b)) : i >= j } )

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

reconsider J = j as Element of NAT by Def3;

defpred S_{1}[ Element of NAT ] means ex k being Element of NAT st $1 = 2 * k;

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

reconsider J = j as Element of NAT by Def3;

defpred S

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

end;

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

end;

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

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

end;

suppose A5:
S_{1}[J]
; :: thesis: x in { ((Net-Str (a,b)) . i) where i is Element of (Net-Str (a,b)) : i >= j }

A6: (Net-Str (a,b)) . j =
((a,b) ,...) . j
by Def3

.= a by A5, Def1 ;

j <= j ;

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

end;.= a by A5, Def1 ;

j <= j ;

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

suppose A7:
not S_{1}[J]
; :: thesis: x in { ((Net-Str (a,b)) . i) where i is Element of (Net-Str (a,b)) : i >= j }

A8: (Net-Str (a,b)) . j =
((a,b) ,...) . j
by Def3

.= b by A7, Def1 ;

reconsider k = J + 1 as Element of (Net-Str (a,b)) by Def3;

A9: (Net-Str (a,b)) . k = a by A8, Th6;

J + 1 >= J by NAT_1:11;

then k >= j by Def3;

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

end;.= b by A7, Def1 ;

reconsider k = J + 1 as Element of (Net-Str (a,b)) by Def3;

A9: (Net-Str (a,b)) . k = a by A8, Th6;

J + 1 >= J by NAT_1:11;

then k >= j by Def3;

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

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

end;

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

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

end;

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

A12: (Net-Str (a,b)) . j =
((a,b) ,...) . j
by Def3

.= b by A11, Def1 ;

j <= j ;

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

end;.= b by A11, Def1 ;

j <= j ;

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

suppose A13:
S_{1}[J]
; :: thesis: x in { ((Net-Str (a,b)) . i) where i is Element of (Net-Str (a,b)) : i >= j }

A14: (Net-Str (a,b)) . j =
((a,b) ,...) . j
by Def3

.= a by A13, Def1 ;

reconsider k = J + 1 as Element of (Net-Str (a,b)) by Def3;

A15: (Net-Str (a,b)) . k = b by A14, Th6;

J + 1 >= J by NAT_1:11;

then k >= j by Def3;

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

end;.= a by A13, Def1 ;

reconsider k = J + 1 as Element of (Net-Str (a,b)) by Def3;

A15: (Net-Str (a,b)) . k = b by A14, Th6;

J + 1 >= J by NAT_1:11;

then k >= j by Def3;

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

deffunc H

defpred S

deffunc H

deffunc H

deffunc H

deffunc H

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

proof

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

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

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

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

end;H

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

hence H

A18: { (a "/\" b) where j4 is Element of (Net-Str (a,b)) : S

proof

{(a "/\" b)} c= { (a "/\" b) where j4 is Element of (Net-Str (a,b)) : S
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (a "/\" b) where j4 is Element of (Net-Str (a,b)) : S_{2}[j4] } or x in {(a "/\" b)} )

assume x in { (a "/\" b) where j4 is Element of (Net-Str (a,b)) : S_{2}[j4] }
; :: thesis: x in {(a "/\" b)}

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

( x = a "/\" b & S_{2}[q] )
;

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

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

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

( x = a "/\" b & S

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

proof

then
{ (a "/\" b) where j4 is Element of (Net-Str (a,b)) : S
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(a "/\" b)} or x in { (a "/\" b) where j4 is Element of (Net-Str (a,b)) : S_{2}[j4] } )

assume x in {(a "/\" b)} ; :: thesis: x in { (a "/\" b) where j4 is Element of (Net-Str (a,b)) : S_{2}[j4] }

then x = a "/\" b by TARSKI:def 1;

hence x in { (a "/\" b) where j4 is Element of (Net-Str (a,b)) : S_{2}[j4] }
; :: thesis: verum

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

then x = a "/\" b by TARSKI:def 1;

hence x in { (a "/\" b) where j4 is Element of (Net-Str (a,b)) : S

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