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 set ; :: 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 & 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 set ; :: 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

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 }

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

end;

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

A7: (Net-Str a,b) . j = (a,b ,... ) . j by Def3
.= b by A6, Def1 ;
reconsider k = J + 1 as Element of (Net-Str a,b) by Def3;
A8: (Net-Str a,b) . k = a by A7, 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, A8; :: 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 A9: x = b ; :: thesis: x in { ((Net-Str a,b) . i) where i is Element of (Net-Str a,b) : i >= j }

now

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

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

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

end;

suppose A11: 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
.= a by A11, Def1 ;
reconsider k = J + 1 as Element of (Net-Str a,b) by Def3;
A13: (Net-Str a,b) . k = b by A12, 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 A9, A13; :: 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 bool 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;
A14: 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;

A15: { 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(A14);
{ (a "/\" b) where j4 is Element of (Net-Str a,b) : S₂[j4] } = {(a "/\" b)}

proof

thus { (a "/\" b) where j4 is Element of (Net-Str a,b) : S₂[j4] } c= {(a "/\" b)} :: according to XBOOLE_0:def 10 :: thesis: {(a "/\" b)} c= { (a "/\" b) where j4 is Element of (Net-Str a,b) : S₂[j4] }

proof

let x be set ; :: 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 consider q being Element of (Net-Str a,b) such that
A16: ( x = a "/\" b & S₂[q] ) ;
thus x in {(a "/\" b)} by A16, TARSKI:def 1; :: thesis: verum

end;

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

proof

let x be set ; :: 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;

end;

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