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 S1[ 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 ( S1[J] or not S1[J] ) ;
suppose A5: S1[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 S1[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 S1[J] or S1[J] ) ;
suppose A11: not S1[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: S1[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 S1[ Element of (Net-Str (a,b)), Element of (Net-Str (a,b))] means $1 >= $2;
deffunc H1( Element of (Net-Str (a,b))) -> set = { ((Net-Str (a,b)) . i1) where i1 is Element of (Net-Str (a,b)) : S1[i1,$1] } ;
defpred S2[ set ] means verum;
deffunc H2( Element of (Net-Str (a,b))) -> Element of K32( the carrier of S) = {a,b};
deffunc H3( Element of (Net-Str (a,b))) -> Element of the carrier of S = "/\" (H1($1),S);
deffunc H4( Element of (Net-Str (a,b))) -> Element of the carrier of S = "/\" (H2($1),S);
deffunc H5( set ) -> Element of the carrier of S = a "/\" b;
A16: for jj being Element of (Net-Str (a,b)) holds H3(jj) = H5(jj)
proof
let jj be Element of (Net-Str (a,b)); :: thesis: H3(jj) = H5(jj)
H3(jj) = H4(jj) by A1
.= a "/\" b by YELLOW_0:40 ;
hence H3(jj) = H5(jj) ; :: thesis: verum
end;
A17: { H3(j3) where j3 is Element of (Net-Str (a,b)) : S2[j3] } = { H5(j4) where j4 is Element of (Net-Str (a,b)) : S2[j4] } from FRAENKEL:sch 5(A16);
 A18: { (a "/\" b) where j4 is Element of (Net-Str (a,b)) : S2[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)) : S2[j4] } or x in {(a "/\" b)} )
assume x in { (a "/\" b) where j4 is Element of (Net-Str (a,b)) : S2[j4] } ; :: thesis: x in {(a "/\" b)}
then ex q being Element of (Net-Str (a,b)) st
( x = a "/\" b & S2[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)) : S2[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)) : S2[j4] } )
assume x in {(a "/\" b)} ; :: thesis: x in { (a "/\" b) where j4 is Element of (Net-Str (a,b)) : S2[j4] }
then x = a "/\" b by TARSKI:def 1;
hence x in { (a "/\" b) where j4 is Element of (Net-Str (a,b)) : S2[j4] } ; :: thesis: verum
end;
then { (a "/\" b) where j4 is Element of (Net-Str (a,b)) : S2[j4] } = {(a "/\" b)} by A18;
hence lim_inf (Net-Str (a,b)) = a "/\" b by A17, YELLOW_0:39; :: thesis: verum