:: RINFSUP2 semantic presentation begin theorem :: RINFSUP2:1 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Var "Y"))) & (Bool (Set (Var "Y")) "is" ($#v4_xxreal_2 :::"bounded_above"::: ) )) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v4_xxreal_2 :::"bounded_above"::: ) ) & (Bool (Set ($#k8_supinf_2 :::"sup"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k4_seq_4 :::"upper_bound"::: ) (Set (Var "Y")))) ")" ))) ; theorem :: RINFSUP2:2 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Var "Y"))) & (Bool (Set (Var "X")) "is" ($#v4_xxreal_2 :::"bounded_above"::: ) )) "holds" (Bool "(" (Bool (Set (Var "Y")) "is" ($#v4_xxreal_2 :::"bounded_above"::: ) ) & (Bool (Set ($#k8_supinf_2 :::"sup"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k4_seq_4 :::"upper_bound"::: ) (Set (Var "Y")))) ")" ))) ; theorem :: RINFSUP2:3 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Var "Y"))) & (Bool (Set (Var "Y")) "is" ($#v3_xxreal_2 :::"bounded_below"::: ) )) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v3_xxreal_2 :::"bounded_below"::: ) ) & (Bool (Set ($#k7_supinf_2 :::"inf"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k5_seq_4 :::"lower_bound"::: ) (Set (Var "Y")))) ")" ))) ; theorem :: RINFSUP2:4 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Var "Y"))) & (Bool (Set (Var "X")) "is" ($#v3_xxreal_2 :::"bounded_below"::: ) )) "holds" (Bool "(" (Bool (Set (Var "Y")) "is" ($#v3_xxreal_2 :::"bounded_below"::: ) ) & (Bool (Set ($#k7_supinf_2 :::"inf"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k5_seq_4 :::"lower_bound"::: ) (Set (Var "Y")))) ")" ))) ; definitionlet "seq" be ($#m1_subset_1 :::"ExtREAL_sequence":::); func :::"sup"::: "seq" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) equals :: RINFSUP2:def 1 (Set ($#k8_supinf_2 :::"sup"::: ) (Set "(" ($#k17_supinf_2 :::"rng"::: ) "seq" ")" )); func :::"inf"::: "seq" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) equals :: RINFSUP2:def 2 (Set ($#k7_supinf_2 :::"inf"::: ) (Set "(" ($#k17_supinf_2 :::"rng"::: ) "seq" ")" )); end; :: deftheorem defines :::"sup"::: RINFSUP2:def 1 : (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "holds" (Bool (Set ($#k1_rinfsup2 :::"sup"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set ($#k8_supinf_2 :::"sup"::: ) (Set "(" ($#k17_supinf_2 :::"rng"::: ) (Set (Var "seq")) ")" )))); :: deftheorem defines :::"inf"::: RINFSUP2:def 2 : (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "holds" (Bool (Set ($#k2_rinfsup2 :::"inf"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set ($#k7_supinf_2 :::"inf"::: ) (Set "(" ($#k17_supinf_2 :::"rng"::: ) (Set (Var "seq")) ")" )))); definitionlet "seq" be ($#m1_subset_1 :::"ExtREAL_sequence":::); attr "seq" is :::"bounded_below"::: means :: RINFSUP2:def 3 (Bool (Set ($#k17_supinf_2 :::"rng"::: ) "seq") "is" ($#v3_xxreal_2 :::"bounded_below"::: ) ); attr "seq" is :::"bounded_above"::: means :: RINFSUP2:def 4 (Bool (Set ($#k17_supinf_2 :::"rng"::: ) "seq") "is" ($#v4_xxreal_2 :::"bounded_above"::: ) ); end; :: deftheorem defines :::"bounded_below"::: RINFSUP2:def 3 : (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v1_rinfsup2 :::"bounded_below"::: ) ) "iff" (Bool (Set ($#k17_supinf_2 :::"rng"::: ) (Set (Var "seq"))) "is" ($#v3_xxreal_2 :::"bounded_below"::: ) ) ")" )); :: deftheorem defines :::"bounded_above"::: RINFSUP2:def 4 : (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v2_rinfsup2 :::"bounded_above"::: ) ) "iff" (Bool (Set ($#k17_supinf_2 :::"rng"::: ) (Set (Var "seq"))) "is" ($#v4_xxreal_2 :::"bounded_above"::: ) ) ")" )); definitionlet "seq" be ($#m1_subset_1 :::"ExtREAL_sequence":::); attr "seq" is :::"bounded"::: means :: RINFSUP2:def 5 (Bool "(" (Bool "seq" "is" ($#v2_rinfsup2 :::"bounded_above"::: ) ) & (Bool "seq" "is" ($#v1_rinfsup2 :::"bounded_below"::: ) ) ")" ); end; :: deftheorem defines :::"bounded"::: RINFSUP2:def 5 : (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v3_rinfsup2 :::"bounded"::: ) ) "iff" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v2_rinfsup2 :::"bounded_above"::: ) ) & (Bool (Set (Var "seq")) "is" ($#v1_rinfsup2 :::"bounded_below"::: ) ) ")" ) ")" )); theorem :: RINFSUP2:5 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "{" (Set "(" (Set (Var "seq")) ($#k12_supinf_2 :::"."::: ) (Set (Var "k")) ")" ) where k "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) "}" "is" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) )))) ; definitionlet "seq" be ($#m1_subset_1 :::"ExtREAL_sequence":::); func :::"inferior_realsequence"::: "seq" -> ($#m1_subset_1 :::"ExtREAL_sequence":::) means :: RINFSUP2:def 6 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "ex" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool "(" (Bool (Set (Var "Y")) ($#r1_hidden :::"="::: ) "{" (Set "(" "seq" ($#k12_supinf_2 :::"."::: ) (Set (Var "k")) ")" ) where k "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) "}" ) & (Bool (Set it ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k7_supinf_2 :::"inf"::: ) (Set (Var "Y")))) ")" ))); end; :: deftheorem defines :::"inferior_realsequence"::: RINFSUP2:def 6 : (Bool "for" (Set (Var "seq")) "," (Set (Var "b2")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k3_rinfsup2 :::"inferior_realsequence"::: ) (Set (Var "seq")))) "iff" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "ex" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool "(" (Bool (Set (Var "Y")) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "seq")) ($#k12_supinf_2 :::"."::: ) (Set (Var "k")) ")" ) where k "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) "}" ) & (Bool (Set (Set (Var "b2")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k7_supinf_2 :::"inf"::: ) (Set (Var "Y")))) ")" ))) ")" )); definitionlet "seq" be ($#m1_subset_1 :::"ExtREAL_sequence":::); func :::"superior_realsequence"::: "seq" -> ($#m1_subset_1 :::"ExtREAL_sequence":::) means :: RINFSUP2:def 7 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "ex" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool "(" (Bool (Set (Var "Y")) ($#r1_hidden :::"="::: ) "{" (Set "(" "seq" ($#k12_supinf_2 :::"."::: ) (Set (Var "k")) ")" ) where k "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) "}" ) & (Bool (Set it ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k8_supinf_2 :::"sup"::: ) (Set (Var "Y")))) ")" ))); end; :: deftheorem defines :::"superior_realsequence"::: RINFSUP2:def 7 : (Bool "for" (Set (Var "seq")) "," (Set (Var "b2")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k4_rinfsup2 :::"superior_realsequence"::: ) (Set (Var "seq")))) "iff" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "ex" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool "(" (Bool (Set (Var "Y")) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "seq")) ($#k12_supinf_2 :::"."::: ) (Set (Var "k")) ")" ) where k "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) "}" ) & (Bool (Set (Set (Var "b2")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k8_supinf_2 :::"sup"::: ) (Set (Var "Y")))) ")" ))) ")" )); theorem :: RINFSUP2:6 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v3_valued_0 :::"real-valued"::: ) )) "holds" (Bool (Set (Var "seq")) "is" ($#m1_subset_1 :::"Real_Sequence":::))) ; theorem :: RINFSUP2:7 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "seq")) "is" ($#v5_valued_0 :::"increasing"::: ) )) "implies" (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "seq")) ($#k12_supinf_2 :::"."::: ) (Set (Var "m"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "seq")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))))) ")" & "(" (Bool (Bool "(" "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "seq")) ($#k12_supinf_2 :::"."::: ) (Set (Var "m"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "seq")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n")))) ")" )) "implies" (Bool (Set (Var "seq")) "is" ($#v5_valued_0 :::"increasing"::: ) ) ")" & "(" (Bool (Bool (Set (Var "seq")) "is" ($#v6_valued_0 :::"decreasing"::: ) )) "implies" (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "seq")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "seq")) ($#k12_supinf_2 :::"."::: ) (Set (Var "m"))))) ")" & "(" (Bool (Bool "(" "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "seq")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "seq")) ($#k12_supinf_2 :::"."::: ) (Set (Var "m")))) ")" )) "implies" (Bool (Set (Var "seq")) "is" ($#v6_valued_0 :::"decreasing"::: ) ) ")" & "(" (Bool (Bool (Set (Var "seq")) "is" ($#v7_valued_0 :::"non-decreasing"::: ) )) "implies" (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "seq")) ($#k12_supinf_2 :::"."::: ) (Set (Var "m"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "seq")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))))) ")" & "(" (Bool (Bool "(" "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "seq")) ($#k12_supinf_2 :::"."::: ) (Set (Var "m"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "seq")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n")))) ")" )) "implies" (Bool (Set (Var "seq")) "is" ($#v7_valued_0 :::"non-decreasing"::: ) ) ")" & "(" (Bool (Bool (Set (Var "seq")) "is" ($#v8_valued_0 :::"non-increasing"::: ) )) "implies" (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "seq")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "seq")) ($#k12_supinf_2 :::"."::: ) (Set (Var "m"))))) ")" & "(" (Bool (Bool "(" "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "seq")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "seq")) ($#k12_supinf_2 :::"."::: ) (Set (Var "m")))) ")" )) "implies" (Bool (Set (Var "seq")) "is" ($#v8_valued_0 :::"non-increasing"::: ) ) ")" ")" )) ; theorem :: RINFSUP2:8 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "holds" (Bool "(" (Bool (Set (Set "(" ($#k3_rinfsup2 :::"inferior_realsequence"::: ) (Set (Var "seq")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "seq")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Set (Var "seq")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k4_rinfsup2 :::"superior_realsequence"::: ) (Set (Var "seq")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "n")))) ")" ))) ; registrationlet "seq" be ($#m1_subset_1 :::"ExtREAL_sequence":::); cluster (Set ($#k4_rinfsup2 :::"superior_realsequence"::: ) "seq") -> ($#v8_valued_0 :::"non-increasing"::: ) ; cluster (Set ($#k3_rinfsup2 :::"inferior_realsequence"::: ) "seq") -> ($#v7_valued_0 :::"non-decreasing"::: ) ; end; definitionlet "seq" be ($#m1_subset_1 :::"ExtREAL_sequence":::); func :::"lim_sup"::: "seq" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) equals :: RINFSUP2:def 8 (Set ($#k2_rinfsup2 :::"inf"::: ) (Set "(" ($#k4_rinfsup2 :::"superior_realsequence"::: ) "seq" ")" )); func :::"lim_inf"::: "seq" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) equals :: RINFSUP2:def 9 (Set ($#k1_rinfsup2 :::"sup"::: ) (Set "(" ($#k3_rinfsup2 :::"inferior_realsequence"::: ) "seq" ")" )); end; :: deftheorem defines :::"lim_sup"::: RINFSUP2:def 8 : (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "holds" (Bool (Set ($#k5_rinfsup2 :::"lim_sup"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set ($#k2_rinfsup2 :::"inf"::: ) (Set "(" ($#k4_rinfsup2 :::"superior_realsequence"::: ) (Set (Var "seq")) ")" )))); :: deftheorem defines :::"lim_inf"::: RINFSUP2:def 9 : (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "holds" (Bool (Set ($#k6_rinfsup2 :::"lim_inf"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set ($#k1_rinfsup2 :::"sup"::: ) (Set "(" ($#k3_rinfsup2 :::"inferior_realsequence"::: ) (Set (Var "seq")) ")" )))); theorem :: RINFSUP2:9 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) (Bool "for" (Set (Var "rseq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) ($#r1_funct_2 :::"="::: ) (Set (Var "rseq"))) & (Bool (Set (Var "rseq")) "is" ($#v1_comseq_2 :::"bounded"::: ) )) "holds" (Bool "(" (Bool (Set ($#k4_rinfsup2 :::"superior_realsequence"::: ) (Set (Var "seq"))) ($#r1_funct_2 :::"="::: ) (Set ($#k4_rinfsup1 :::"superior_realsequence"::: ) (Set (Var "rseq")))) & (Bool (Set ($#k5_rinfsup2 :::"lim_sup"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set ($#k5_rinfsup1 :::"lim_sup"::: ) (Set (Var "rseq")))) ")" ))) ; theorem :: RINFSUP2:10 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) (Bool "for" (Set (Var "rseq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) ($#r1_funct_2 :::"="::: ) (Set (Var "rseq"))) & (Bool (Set (Var "rseq")) "is" ($#v1_comseq_2 :::"bounded"::: ) )) "holds" (Bool "(" (Bool (Set ($#k3_rinfsup2 :::"inferior_realsequence"::: ) (Set (Var "seq"))) ($#r1_funct_2 :::"="::: ) (Set ($#k3_rinfsup1 :::"inferior_realsequence"::: ) (Set (Var "rseq")))) & (Bool (Set ($#k6_rinfsup2 :::"lim_inf"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set ($#k6_rinfsup1 :::"lim_inf"::: ) (Set (Var "rseq")))) ")" ))) ; theorem :: RINFSUP2:11 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v3_rinfsup2 :::"bounded"::: ) )) "holds" (Bool (Set (Var "seq")) "is" ($#m1_subset_1 :::"Real_Sequence":::))) ; theorem :: RINFSUP2:12 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) (Bool "for" (Set (Var "rseq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) ($#r1_funct_2 :::"="::: ) (Set (Var "rseq")))) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v2_rinfsup2 :::"bounded_above"::: ) ) "iff" (Bool (Set (Var "rseq")) "is" bbbadV1_SEQ_2()) ")" ))) ; theorem :: RINFSUP2:13 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) (Bool "for" (Set (Var "rseq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) ($#r1_funct_2 :::"="::: ) (Set (Var "rseq")))) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v1_rinfsup2 :::"bounded_below"::: ) ) "iff" (Bool (Set (Var "rseq")) "is" bbbadV2_SEQ_2()) ")" ))) ; theorem :: RINFSUP2:14 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) (Bool "for" (Set (Var "rseq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) ($#r1_funct_2 :::"="::: ) (Set (Var "rseq"))) & (Bool (Set (Var "rseq")) "is" ($#v2_comseq_2 :::"convergent"::: ) )) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v7_mesfunc5 :::"convergent_to_finite_number"::: ) ) & (Bool (Set (Var "seq")) "is" ($#v10_mesfunc5 :::"convergent"::: ) ) & (Bool (Set ($#k2_mesfunc5 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set ($#k2_seq_2 :::"lim"::: ) (Set (Var "rseq")))) ")" ))) ; theorem :: RINFSUP2:15 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) (Bool "for" (Set (Var "rseq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) ($#r1_funct_2 :::"="::: ) (Set (Var "rseq"))) & (Bool (Set (Var "seq")) "is" ($#v7_mesfunc5 :::"convergent_to_finite_number"::: ) )) "holds" (Bool "(" (Bool (Set (Var "rseq")) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_mesfunc5 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set ($#k2_seq_2 :::"lim"::: ) (Set (Var "rseq")))) ")" ))) ; theorem :: RINFSUP2:16 (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "st" (Bool (Bool (Set (Set (Var "seq")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k"))) "is" ($#v7_mesfunc5 :::"convergent_to_finite_number"::: ) )) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v7_mesfunc5 :::"convergent_to_finite_number"::: ) ) & (Bool (Set (Var "seq")) "is" ($#v10_mesfunc5 :::"convergent"::: ) ) & (Bool (Set ($#k2_mesfunc5 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set ($#k2_mesfunc5 :::"lim"::: ) (Set "(" (Set (Var "seq")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k")) ")" ))) ")" ))) ; theorem :: RINFSUP2:17 (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "st" (Bool (Bool (Set (Set (Var "seq")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k"))) "is" ($#v10_mesfunc5 :::"convergent"::: ) )) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v10_mesfunc5 :::"convergent"::: ) ) & (Bool (Set ($#k2_mesfunc5 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set ($#k2_mesfunc5 :::"lim"::: ) (Set "(" (Set (Var "seq")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k")) ")" ))) ")" ))) ; theorem :: RINFSUP2:18 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "st" (Bool (Bool (Set ($#k5_rinfsup2 :::"lim_sup"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set ($#k6_rinfsup2 :::"lim_inf"::: ) (Set (Var "seq")))) & (Bool (Set ($#k6_rinfsup2 :::"lim_inf"::: ) (Set (Var "seq"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_numbers :::"REAL"::: ) ))) "holds" (Bool "ex" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set (Set (Var "seq")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k"))) "is" ($#v3_rinfsup2 :::"bounded"::: ) ))) ; theorem :: RINFSUP2:19 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v7_mesfunc5 :::"convergent_to_finite_number"::: ) )) "holds" (Bool "ex" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set (Set (Var "seq")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k"))) "is" ($#v3_rinfsup2 :::"bounded"::: ) ))) ; theorem :: RINFSUP2:20 (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v7_mesfunc5 :::"convergent_to_finite_number"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "seq")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k"))) "is" ($#v7_mesfunc5 :::"convergent_to_finite_number"::: ) ) & (Bool (Set (Set (Var "seq")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k"))) "is" ($#v10_mesfunc5 :::"convergent"::: ) ) & (Bool (Set ($#k2_mesfunc5 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set ($#k2_mesfunc5 :::"lim"::: ) (Set "(" (Set (Var "seq")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k")) ")" ))) ")" ))) ; theorem :: RINFSUP2:21 (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v10_mesfunc5 :::"convergent"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "seq")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k"))) "is" ($#v10_mesfunc5 :::"convergent"::: ) ) & (Bool (Set ($#k2_mesfunc5 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set ($#k2_mesfunc5 :::"lim"::: ) (Set "(" (Set (Var "seq")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k")) ")" ))) ")" ))) ; theorem :: RINFSUP2:22 (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "seq")) "is" ($#v2_rinfsup2 :::"bounded_above"::: ) )) "implies" (Bool (Set (Set (Var "seq")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k"))) "is" ($#v2_rinfsup2 :::"bounded_above"::: ) ) ")" & "(" (Bool (Bool (Set (Var "seq")) "is" ($#v1_rinfsup2 :::"bounded_below"::: ) )) "implies" (Bool (Set (Set (Var "seq")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k"))) "is" ($#v1_rinfsup2 :::"bounded_below"::: ) ) ")" ")" ))) ; theorem :: RINFSUP2:23 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "holds" (Bool "(" (Bool (Set ($#k2_rinfsup2 :::"inf"::: ) (Set (Var "seq"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "seq")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Set (Var "seq")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_rinfsup2 :::"sup"::: ) (Set (Var "seq")))) ")" ))) ; theorem :: RINFSUP2:24 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "holds" (Bool (Set ($#k2_rinfsup2 :::"inf"::: ) (Set (Var "seq"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_rinfsup2 :::"sup"::: ) (Set (Var "seq"))))) ; theorem :: RINFSUP2:25 (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v8_valued_0 :::"non-increasing"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "seq")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k"))) "is" ($#v8_valued_0 :::"non-increasing"::: ) ) & (Bool (Set ($#k2_rinfsup2 :::"inf"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set ($#k2_rinfsup2 :::"inf"::: ) (Set "(" (Set (Var "seq")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k")) ")" ))) ")" ))) ; theorem :: RINFSUP2:26 (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v7_valued_0 :::"non-decreasing"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "seq")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k"))) "is" ($#v7_valued_0 :::"non-decreasing"::: ) ) & (Bool (Set ($#k1_rinfsup2 :::"sup"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set ($#k1_rinfsup2 :::"sup"::: ) (Set "(" (Set (Var "seq")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k")) ")" ))) ")" ))) ; theorem :: RINFSUP2:27 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "holds" (Bool "(" (Bool (Set (Set "(" ($#k4_rinfsup2 :::"superior_realsequence"::: ) (Set (Var "seq")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k1_rinfsup2 :::"sup"::: ) (Set "(" (Set (Var "seq")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "n")) ")" ))) & (Bool (Set (Set "(" ($#k3_rinfsup2 :::"inferior_realsequence"::: ) (Set (Var "seq")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k2_rinfsup2 :::"inf"::: ) (Set "(" (Set (Var "seq")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "n")) ")" ))) ")" ))) ; theorem :: RINFSUP2:28 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) (Bool "for" (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set ($#k4_rinfsup2 :::"superior_realsequence"::: ) (Set "(" (Set (Var "seq")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "j")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k4_rinfsup2 :::"superior_realsequence"::: ) (Set (Var "seq")) ")" ) ($#k1_valued_0 :::"^\"::: ) (Set (Var "j")))) & (Bool (Set ($#k5_rinfsup2 :::"lim_sup"::: ) (Set "(" (Set (Var "seq")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "j")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_rinfsup2 :::"lim_sup"::: ) (Set (Var "seq")))) ")" ))) ; theorem :: RINFSUP2:29 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) (Bool "for" (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set ($#k3_rinfsup2 :::"inferior_realsequence"::: ) (Set "(" (Set (Var "seq")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "j")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k3_rinfsup2 :::"inferior_realsequence"::: ) (Set (Var "seq")) ")" ) ($#k1_valued_0 :::"^\"::: ) (Set (Var "j")))) & (Bool (Set ($#k6_rinfsup2 :::"lim_inf"::: ) (Set "(" (Set (Var "seq")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "j")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_rinfsup2 :::"lim_inf"::: ) (Set (Var "seq")))) ")" ))) ; theorem :: RINFSUP2:30 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v8_valued_0 :::"non-increasing"::: ) ) & (Bool (Set ($#k2_supinf_1 :::"-infty"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "seq")) ($#k12_supinf_2 :::"."::: ) (Set (Var "k")))) & (Bool (Set (Set (Var "seq")) ($#k12_supinf_2 :::"."::: ) (Set (Var "k"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) ))) "holds" (Bool "(" (Bool (Set (Set (Var "seq")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k"))) "is" ($#v2_rinfsup2 :::"bounded_above"::: ) ) & (Bool (Set ($#k1_rinfsup2 :::"sup"::: ) (Set "(" (Set (Var "seq")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "seq")) ($#k12_supinf_2 :::"."::: ) (Set (Var "k")))) ")" ))) ; theorem :: RINFSUP2:31 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v7_valued_0 :::"non-decreasing"::: ) ) & (Bool (Set ($#k2_supinf_1 :::"-infty"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "seq")) ($#k12_supinf_2 :::"."::: ) (Set (Var "k")))) & (Bool (Set (Set (Var "seq")) ($#k12_supinf_2 :::"."::: ) (Set (Var "k"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) ))) "holds" (Bool "(" (Bool (Set (Set (Var "seq")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k"))) "is" ($#v1_rinfsup2 :::"bounded_below"::: ) ) & (Bool (Set ($#k2_rinfsup2 :::"inf"::: ) (Set "(" (Set (Var "seq")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "seq")) ($#k12_supinf_2 :::"."::: ) (Set (Var "k")))) ")" ))) ; theorem :: RINFSUP2:32 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k1_supinf_1 :::"+infty"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "seq")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n")))) ")" )) "holds" (Bool (Set (Var "seq")) "is" ($#v8_mesfunc5 :::"convergent_to_+infty"::: ) )) ; theorem :: RINFSUP2:33 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "seq")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k2_supinf_1 :::"-infty"::: ) )) ")" )) "holds" (Bool (Set (Var "seq")) "is" ($#v9_mesfunc5 :::"convergent_to_-infty"::: ) )) ; theorem :: RINFSUP2:34 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v8_valued_0 :::"non-increasing"::: ) ) & (Bool (Set ($#k2_supinf_1 :::"-infty"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_rinfsup2 :::"inf"::: ) (Set (Var "seq"))))) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v9_mesfunc5 :::"convergent_to_-infty"::: ) ) & (Bool (Set ($#k2_mesfunc5 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set ($#k2_supinf_1 :::"-infty"::: ) )) ")" )) ; theorem :: RINFSUP2:35 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v7_valued_0 :::"non-decreasing"::: ) ) & (Bool (Set ($#k1_supinf_1 :::"+infty"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_rinfsup2 :::"sup"::: ) (Set (Var "seq"))))) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v8_mesfunc5 :::"convergent_to_+infty"::: ) ) & (Bool (Set ($#k2_mesfunc5 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) )) ")" )) ; theorem :: RINFSUP2:36 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v8_valued_0 :::"non-increasing"::: ) )) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v10_mesfunc5 :::"convergent"::: ) ) & (Bool (Set ($#k2_mesfunc5 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set ($#k2_rinfsup2 :::"inf"::: ) (Set (Var "seq")))) ")" )) ; theorem :: RINFSUP2:37 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v7_valued_0 :::"non-decreasing"::: ) )) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v10_mesfunc5 :::"convergent"::: ) ) & (Bool (Set ($#k2_mesfunc5 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set ($#k1_rinfsup2 :::"sup"::: ) (Set (Var "seq")))) ")" )) ; theorem :: RINFSUP2:38 (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "st" (Bool (Bool (Set (Var "seq1")) "is" ($#v10_mesfunc5 :::"convergent"::: ) ) & (Bool (Set (Var "seq2")) "is" ($#v10_mesfunc5 :::"convergent"::: ) ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "seq1")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "seq2")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n")))) ")" )) "holds" (Bool (Set ($#k2_mesfunc5 :::"lim"::: ) (Set (Var "seq1"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k2_mesfunc5 :::"lim"::: ) (Set (Var "seq2"))))) ; theorem :: RINFSUP2:39 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "holds" (Bool (Set ($#k6_rinfsup2 :::"lim_inf"::: ) (Set (Var "seq"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k5_rinfsup2 :::"lim_sup"::: ) (Set (Var "seq"))))) ; theorem :: RINFSUP2:40 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v10_mesfunc5 :::"convergent"::: ) ) "iff" (Bool (Set ($#k6_rinfsup2 :::"lim_inf"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set ($#k5_rinfsup2 :::"lim_sup"::: ) (Set (Var "seq")))) ")" )) ; theorem :: RINFSUP2:41 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v10_mesfunc5 :::"convergent"::: ) )) "holds" (Bool "(" (Bool (Set ($#k2_mesfunc5 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set ($#k6_rinfsup2 :::"lim_inf"::: ) (Set (Var "seq")))) & (Bool (Set ($#k2_mesfunc5 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set ($#k5_rinfsup2 :::"lim_sup"::: ) (Set (Var "seq")))) ")" )) ;