let S be with_infima Poset; :: thesis: for a, b being Element of holds lim_inf (Net-Str a,b) = a "/\" b
let a, b be Element of ; :: thesis: lim_inf (Net-Str a,b) = a "/\" b
set N = Net-Str a,b;
A1: for j being Element of holds { ((Net-Str a,b) . i) where i is Element of : i >= j } = {a,b}

proof

let j be Element of ; :: thesis: { ((Net-Str a,b) . i) where i is Element of : i >= j } = {a,b}
thus { ((Net-Str a,b) . i) where i is Element of : 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 : 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 : i >= j } or x in {a,b} )
assume x in { ((Net-Str a,b) . i) where i is Element of : i >= j } ; :: thesis: x in {a,b}
then consider i1 being Element of 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 : 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 : i >= j } )
assume A3: x in {a,b} ; :: thesis: x in { ((Net-Str a,b) . i) where i is Element of : 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 : 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 : 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 : 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 : i >= j }

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

end;

end;

end;

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

end;

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

now

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 : 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 : 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 : i >= j }

A14: (Net-Str a,b) . j = (a,b ,... ) . j by Def3
.= a by A13, Def1 ;
reconsider k = J + 1 as Element of 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 : i >= j } by A10, A15; :: thesis: verum

end;

end;

end;

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

end;

end;

end;

end;

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

proof

let jj be Element of ; :: 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 : S₂[j3] } = { H₅(j4) where j4 is Element of : S₂[j4] } from FRAENKEL:sch 5(A16);
A18: { (a "/\" b) where j4 is Element of : S₂[j4] } c= {(a "/\" b)}

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (a "/\" b) where j4 is Element of : S₂[j4] } or x in {(a "/\" b)} )
assume x in { (a "/\" b) where j4 is Element of : S₂[j4] } ; :: thesis: x in {(a "/\" b)}
then ex q being Element of 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 : S₂[j4] }

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

end;

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