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}

proof

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 }

proof

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;

thus {a,b} c= { ((Net-Str (a,b)) . i) where i is Element of (Net-Str (a,b)) : i >= j } :: 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₁[ Element of NAT ] means ex k being Element of NAT st $1 = 2 * k;

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

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

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

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

suppose A5: S₁[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;

suppose A7: not S₁[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;

end;

end;

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

end;

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

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

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

suppose A11: not S₁[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;

suppose A13: S₁[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;

end;

end;

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

end;

end;

end;

end;

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

proof

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

end;

A17: { H₃(j3) where j3 is Element of (Net-Str (a,b)) : S₂[j3] } = { H₅(j4) where j4 is Element of (Net-Str (a,b)) : S₂[j4] } from FRAENKEL:sch 5(A16);
A18: { (a "/\" b) where j4 is Element of (Net-Str (a,b)) : S₂[j4] } c= {(a "/\" b)}

proof

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₂[j4] } or x in {(a "/\" b)} )
assume x in { (a "/\" b) where j4 is Element of (Net-Str (a,b)) : S₂[j4] } ; :: thesis: x in {(a "/\" b)}
then ex q being Element of (Net-Str (a,b)) st
( x = a "/\" b & S₂[q] ) ;
hence x in {(a "/\" b)} by TARSKI:def 1; :: thesis: verum

end;

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

proof

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₂[j4] } )
assume x in {(a "/\" b)} ; :: thesis: x in { (a "/\" b) where j4 is Element of (Net-Str (a,b)) : S₂[j4] }
then x = a "/\" b by TARSKI:def 1;
hence x in { (a "/\" b) where j4 is Element of (Net-Str (a,b)) : S₂[j4] } ; :: thesis: verum

end;

then { (a "/\" b) where j4 is Element of (Net-Str (a,b)) : S₂[j4] } = {(a "/\" b)} by A18;
hence lim_inf (Net-Str (a,b)) = a "/\" b by A17, YELLOW_0:39; :: thesis: verum