:: ARYTM_2 semantic presentation begin definitionfunc :::"DEDEKIND_CUTS"::: -> ($#m1_subset_1 :::"Subset-Family":::) "of" (Set ($#k5_arytm_3 :::"RAT+"::: ) ) equals :: ARYTM_2:def 1 (Set "{" (Set (Var "A")) where A "is" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k5_arytm_3 :::"RAT+"::: ) ) : (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_arytm_3 :::"RAT+"::: ) ) "st" (Bool (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool "(" (Bool "(" "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_arytm_3 :::"RAT+"::: ) ) "st" (Bool (Bool (Set (Var "s")) ($#r3_arytm_3 :::"<='"::: ) (Set (Var "r")))) "holds" (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" ) & (Bool "ex" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_arytm_3 :::"RAT+"::: ) ) "st" (Bool "(" (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "r")) ($#r3_arytm_3 :::"<"::: ) (Set (Var "s"))) ")" )) ")" )) "}" ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k5_arytm_3 :::"RAT+"::: ) ) ($#k1_tarski :::"}"::: ) )); end; :: deftheorem defines :::"DEDEKIND_CUTS"::: ARYTM_2:def 1 : (Bool (Set ($#k1_arytm_2 :::"DEDEKIND_CUTS"::: ) ) ($#r1_hidden :::"="::: ) (Set "{" (Set (Var "A")) where A "is" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k5_arytm_3 :::"RAT+"::: ) ) : (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_arytm_3 :::"RAT+"::: ) ) "st" (Bool (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool "(" (Bool "(" "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_arytm_3 :::"RAT+"::: ) ) "st" (Bool (Bool (Set (Var "s")) ($#r3_arytm_3 :::"<='"::: ) (Set (Var "r")))) "holds" (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" ) & (Bool "ex" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_arytm_3 :::"RAT+"::: ) ) "st" (Bool "(" (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "r")) ($#r3_arytm_3 :::"<"::: ) (Set (Var "s"))) ")" )) ")" )) "}" ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k5_arytm_3 :::"RAT+"::: ) ) ($#k1_tarski :::"}"::: ) ))); registration cluster (Set ($#k1_arytm_2 :::"DEDEKIND_CUTS"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionfunc :::"REAL+"::: -> ($#m1_hidden :::"set"::: ) equals :: ARYTM_2:def 2 (Set (Set "(" (Set ($#k5_arytm_3 :::"RAT+"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_arytm_2 :::"DEDEKIND_CUTS"::: ) ) ")" ) ($#k6_subset_1 :::"\"::: ) "{" "{" (Set (Var "s")) where s "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_arytm_3 :::"RAT+"::: ) ) : (Bool (Set (Var "s")) ($#r3_arytm_3 :::"<"::: ) (Set (Var "t"))) "}" where t "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_arytm_3 :::"RAT+"::: ) ) : (Bool (Set (Var "t")) ($#r1_hidden :::"<>"::: ) (Set ($#k11_arytm_3 :::"{}"::: ) )) "}" ); end; :: deftheorem defines :::"REAL+"::: ARYTM_2:def 2 : (Bool (Set ($#k2_arytm_2 :::"REAL+"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k5_arytm_3 :::"RAT+"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_arytm_2 :::"DEDEKIND_CUTS"::: ) ) ")" ) ($#k6_subset_1 :::"\"::: ) "{" "{" (Set (Var "s")) where s "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_arytm_3 :::"RAT+"::: ) ) : (Bool (Set (Var "s")) ($#r3_arytm_3 :::"<"::: ) (Set (Var "t"))) "}" where t "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_arytm_3 :::"RAT+"::: ) ) : (Bool (Set (Var "t")) ($#r1_hidden :::"<>"::: ) (Set ($#k11_arytm_3 :::"{}"::: ) )) "}" )); theorem :: ARYTM_2:1 (Bool (Set ($#k5_arytm_3 :::"RAT+"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k2_arytm_2 :::"REAL+"::: ) )) ; theorem :: ARYTM_2:2 (Bool (Set ($#k4_ordinal1 :::"omega"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k2_arytm_2 :::"REAL+"::: ) )) ; registration cluster (Set ($#k2_arytm_2 :::"REAL+"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ); func :::"DEDEKIND_CUT"::: "x" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_arytm_2 :::"DEDEKIND_CUTS"::: ) ) means :: ARYTM_2:def 3 (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_arytm_3 :::"RAT+"::: ) ) "st" (Bool "(" (Bool "x" ($#r1_hidden :::"="::: ) (Set (Var "r"))) & (Bool it ($#r1_hidden :::"="::: ) "{" (Set (Var "s")) where s "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_arytm_3 :::"RAT+"::: ) ) : (Bool (Set (Var "s")) ($#r3_arytm_3 :::"<"::: ) (Set (Var "r"))) "}" ) ")" )) if (Bool "x" ($#r2_hidden :::"in"::: ) (Set ($#k5_arytm_3 :::"RAT+"::: ) )) otherwise (Bool it ($#r1_hidden :::"="::: ) "x"); end; :: deftheorem defines :::"DEDEKIND_CUT"::: ARYTM_2:def 3 : (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) (Bool "for" (Set (Var "b2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_arytm_2 :::"DEDEKIND_CUTS"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k5_arytm_3 :::"RAT+"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k3_arytm_2 :::"DEDEKIND_CUT"::: ) (Set (Var "x")))) "iff" (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_arytm_3 :::"RAT+"::: ) ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "r"))) & (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) "{" (Set (Var "s")) where s "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_arytm_3 :::"RAT+"::: ) ) : (Bool (Set (Var "s")) ($#r3_arytm_3 :::"<"::: ) (Set (Var "r"))) "}" ) ")" )) ")" ) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k5_arytm_3 :::"RAT+"::: ) )))) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k3_arytm_2 :::"DEDEKIND_CUT"::: ) (Set (Var "x")))) "iff" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" ) ")" ")" ))); theorem :: ARYTM_2:3 (Bool "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Bool "not" (Set ($#k4_tarski :::"["::: ) (Set ($#k11_arytm_3 :::"{}"::: ) ) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_arytm_2 :::"REAL+"::: ) )))) ; definitionlet "x" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_arytm_2 :::"DEDEKIND_CUTS"::: ) ); func :::"GLUED"::: "x" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) means :: ARYTM_2:def 4 (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_arytm_3 :::"RAT+"::: ) ) "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set (Var "r"))) & (Bool "(" "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_arytm_3 :::"RAT+"::: ) ) "holds" (Bool "(" (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) "x") "iff" (Bool (Set (Var "s")) ($#r3_arytm_3 :::"<"::: ) (Set (Var "r"))) ")" ) ")" ) ")" )) if (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_arytm_3 :::"RAT+"::: ) ) "st" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_arytm_3 :::"RAT+"::: ) ) "holds" (Bool "(" (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) "x") "iff" (Bool (Set (Var "s")) ($#r3_arytm_3 :::"<"::: ) (Set (Var "r"))) ")" ))) otherwise (Bool it ($#r1_hidden :::"="::: ) "x"); end; :: deftheorem defines :::"GLUED"::: ARYTM_2:def 4 : (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_arytm_2 :::"DEDEKIND_CUTS"::: ) ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) "holds" (Bool "(" "(" (Bool (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_arytm_3 :::"RAT+"::: ) ) "st" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_arytm_3 :::"RAT+"::: ) ) "holds" (Bool "(" (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set (Var "x"))) "iff" (Bool (Set (Var "s")) ($#r3_arytm_3 :::"<"::: ) (Set (Var "r"))) ")" )))) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k4_arytm_2 :::"GLUED"::: ) (Set (Var "x")))) "iff" (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_arytm_3 :::"RAT+"::: ) ) "st" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Var "r"))) & (Bool "(" "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_arytm_3 :::"RAT+"::: ) ) "holds" (Bool "(" (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set (Var "x"))) "iff" (Bool (Set (Var "s")) ($#r3_arytm_3 :::"<"::: ) (Set (Var "r"))) ")" ) ")" ) ")" )) ")" ) ")" & "(" (Bool (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_arytm_3 :::"RAT+"::: ) ) "holds" (Bool "not" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_arytm_3 :::"RAT+"::: ) ) "holds" (Bool "(" (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set (Var "x"))) "iff" (Bool (Set (Var "s")) ($#r3_arytm_3 :::"<"::: ) (Set (Var "r"))) ")" ))) ")" )) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k4_arytm_2 :::"GLUED"::: ) (Set (Var "x")))) "iff" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" ) ")" ")" ))); definitionlet "x", "y" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ); pred "x" :::"<='"::: "y" means :: ARYTM_2:def 5 (Bool "ex" (Set (Var "x9")) "," (Set (Var "y9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_arytm_3 :::"RAT+"::: ) ) "st" (Bool "(" (Bool "x" ($#r1_hidden :::"="::: ) (Set (Var "x9"))) & (Bool "y" ($#r1_hidden :::"="::: ) (Set (Var "y9"))) & (Bool (Set (Var "x9")) ($#r3_arytm_3 :::"<='"::: ) (Set (Var "y9"))) ")" )) if (Bool "(" (Bool "x" ($#r2_hidden :::"in"::: ) (Set ($#k5_arytm_3 :::"RAT+"::: ) )) & (Bool "y" ($#r2_hidden :::"in"::: ) (Set ($#k5_arytm_3 :::"RAT+"::: ) )) ")" ) (Bool "x" ($#r2_hidden :::"in"::: ) "y") if (Bool "(" (Bool "x" ($#r2_hidden :::"in"::: ) (Set ($#k5_arytm_3 :::"RAT+"::: ) )) & (Bool (Bool "not" "y" ($#r2_hidden :::"in"::: ) (Set ($#k5_arytm_3 :::"RAT+"::: ) ))) ")" ) (Bool (Bool "not" "y" ($#r2_hidden :::"in"::: ) "x")) if (Bool "(" (Bool (Bool "not" "x" ($#r2_hidden :::"in"::: ) (Set ($#k5_arytm_3 :::"RAT+"::: ) ))) & (Bool "y" ($#r2_hidden :::"in"::: ) (Set ($#k5_arytm_3 :::"RAT+"::: ) )) ")" ) otherwise (Bool "x" ($#r1_tarski :::"c="::: ) "y"); connectedness (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) "st" (Bool (Bool "(" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k5_arytm_3 :::"RAT+"::: ) )) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k5_arytm_3 :::"RAT+"::: ) )) & (Bool "(" "for" (Set (Var "x9")) "," (Set (Var "y9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_arytm_3 :::"RAT+"::: ) ) "holds" (Bool "(" "not" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x9"))) "or" "not" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "y9"))) "or" "not" (Bool (Set (Var "x9")) ($#r3_arytm_3 :::"<='"::: ) (Set (Var "y9"))) ")" ) ")" ) ")" ) "or" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k5_arytm_3 :::"RAT+"::: ) )) & (Bool (Bool "not" (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k5_arytm_3 :::"RAT+"::: ) ))) & (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "y")))) ")" ) "or" (Bool "(" (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k5_arytm_3 :::"RAT+"::: ) ))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k5_arytm_3 :::"RAT+"::: ) )) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "x"))) ")" ) "or" (Bool "(" (Bool "(" "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k5_arytm_3 :::"RAT+"::: ) )) "or" "not" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k5_arytm_3 :::"RAT+"::: ) )) ")" ) & (Bool "(" "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k5_arytm_3 :::"RAT+"::: ) )) "or" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k5_arytm_3 :::"RAT+"::: ) )) ")" ) & (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k5_arytm_3 :::"RAT+"::: ) )) "or" "not" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k5_arytm_3 :::"RAT+"::: ) )) ")" ) & (Bool (Bool "not" (Set (Var "x")) ($#r1_tarski :::"c="::: ) (Set (Var "y")))) ")" ) ")" )) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k5_arytm_3 :::"RAT+"::: ) )) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k5_arytm_3 :::"RAT+"::: ) ))) "implies" (Bool "ex" (Set (Var "x9")) "," (Set (Var "y9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_arytm_3 :::"RAT+"::: ) ) "st" (Bool "(" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "x9"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y9"))) & (Bool (Set (Var "x9")) ($#r3_arytm_3 :::"<='"::: ) (Set (Var "y9"))) ")" )) ")" & "(" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k5_arytm_3 :::"RAT+"::: ) )) & (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k5_arytm_3 :::"RAT+"::: ) )))) "implies" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "x"))) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k5_arytm_3 :::"RAT+"::: ) ))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k5_arytm_3 :::"RAT+"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "y")))) ")" & "(" (Bool (Bool "(" "not" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k5_arytm_3 :::"RAT+"::: ) )) "or" "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k5_arytm_3 :::"RAT+"::: ) )) ")" ) & (Bool "(" "not" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k5_arytm_3 :::"RAT+"::: ) )) "or" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k5_arytm_3 :::"RAT+"::: ) )) ")" ) & (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k5_arytm_3 :::"RAT+"::: ) )) "or" "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k5_arytm_3 :::"RAT+"::: ) )) ")" )) "implies" (Bool (Set (Var "y")) ($#r1_tarski :::"c="::: ) (Set (Var "x"))) ")" ")" )) ; end; :: deftheorem defines :::"<='"::: ARYTM_2:def 5 : (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k5_arytm_3 :::"RAT+"::: ) )) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k5_arytm_3 :::"RAT+"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "x")) ($#r1_arytm_2 :::"<='"::: ) (Set (Var "y"))) "iff" (Bool "ex" (Set (Var "x9")) "," (Set (Var "y9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_arytm_3 :::"RAT+"::: ) ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x9"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "y9"))) & (Bool (Set (Var "x9")) ($#r3_arytm_3 :::"<='"::: ) (Set (Var "y9"))) ")" )) ")" ) ")" & "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k5_arytm_3 :::"RAT+"::: ) )) & (Bool (Bool "not" (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k5_arytm_3 :::"RAT+"::: ) )))) "implies" (Bool "(" (Bool (Set (Var "x")) ($#r1_arytm_2 :::"<='"::: ) (Set (Var "y"))) "iff" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "y"))) ")" ) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k5_arytm_3 :::"RAT+"::: ) ))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k5_arytm_3 :::"RAT+"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "x")) ($#r1_arytm_2 :::"<='"::: ) (Set (Var "y"))) "iff" (Bool (Bool "not" (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "x")))) ")" ) ")" & "(" (Bool (Bool "(" "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k5_arytm_3 :::"RAT+"::: ) )) "or" "not" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k5_arytm_3 :::"RAT+"::: ) )) ")" ) & (Bool "(" "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k5_arytm_3 :::"RAT+"::: ) )) "or" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k5_arytm_3 :::"RAT+"::: ) )) ")" ) & (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k5_arytm_3 :::"RAT+"::: ) )) "or" "not" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k5_arytm_3 :::"RAT+"::: ) )) ")" )) "implies" (Bool "(" (Bool (Set (Var "x")) ($#r1_arytm_2 :::"<='"::: ) (Set (Var "y"))) "iff" (Bool (Set (Var "x")) ($#r1_tarski :::"c="::: ) (Set (Var "y"))) ")" ) ")" ")" )); notationlet "x", "y" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ); antonym "y" :::"<"::: "x" for "x" :::"<='"::: "y"; end; definitionlet "A", "B" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_arytm_2 :::"DEDEKIND_CUTS"::: ) ); func "A" :::"+"::: "B" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_arytm_2 :::"DEDEKIND_CUTS"::: ) ) equals :: ARYTM_2:def 6 "{" (Set "(" (Set (Var "r")) ($#k9_arytm_3 :::"+"::: ) (Set (Var "s")) ")" ) where r, s "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_arytm_3 :::"RAT+"::: ) ) : (Bool "(" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) "A") & (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) "B") ")" ) "}" ; commutativity (Bool "for" (Set (Var "b1")) "," (Set (Var "A")) "," (Set (Var "B")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_arytm_2 :::"DEDEKIND_CUTS"::: ) ) "st" (Bool (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "r")) ($#k9_arytm_3 :::"+"::: ) (Set (Var "s")) ")" ) where r, s "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_arytm_3 :::"RAT+"::: ) ) : (Bool "(" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) ")" ) "}" )) "holds" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "r")) ($#k9_arytm_3 :::"+"::: ) (Set (Var "s")) ")" ) where r, s "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_arytm_3 :::"RAT+"::: ) ) : (Bool "(" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" ) "}" )) ; end; :: deftheorem defines :::"+"::: ARYTM_2:def 6 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_arytm_2 :::"DEDEKIND_CUTS"::: ) ) "holds" (Bool (Set (Set (Var "A")) ($#k5_arytm_2 :::"+"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "r")) ($#k9_arytm_3 :::"+"::: ) (Set (Var "s")) ")" ) where r, s "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_arytm_3 :::"RAT+"::: ) ) : (Bool "(" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) ")" ) "}" )); definitionlet "A", "B" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_arytm_2 :::"DEDEKIND_CUTS"::: ) ); func "A" :::"*'"::: "B" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_arytm_2 :::"DEDEKIND_CUTS"::: ) ) equals :: ARYTM_2:def 7 "{" (Set "(" (Set (Var "r")) ($#k10_arytm_3 :::"*'"::: ) (Set (Var "s")) ")" ) where r, s "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_arytm_3 :::"RAT+"::: ) ) : (Bool "(" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) "A") & (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) "B") ")" ) "}" ; commutativity (Bool "for" (Set (Var "b1")) "," (Set (Var "A")) "," (Set (Var "B")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_arytm_2 :::"DEDEKIND_CUTS"::: ) ) "st" (Bool (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "r")) ($#k10_arytm_3 :::"*'"::: ) (Set (Var "s")) ")" ) where r, s "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_arytm_3 :::"RAT+"::: ) ) : (Bool "(" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) ")" ) "}" )) "holds" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "r")) ($#k10_arytm_3 :::"*'"::: ) (Set (Var "s")) ")" ) where r, s "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_arytm_3 :::"RAT+"::: ) ) : (Bool "(" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" ) "}" )) ; end; :: deftheorem defines :::"*'"::: ARYTM_2:def 7 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_arytm_2 :::"DEDEKIND_CUTS"::: ) ) "holds" (Bool (Set (Set (Var "A")) ($#k6_arytm_2 :::"*'"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "r")) ($#k10_arytm_3 :::"*'"::: ) (Set (Var "s")) ")" ) where r, s "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_arytm_3 :::"RAT+"::: ) ) : (Bool "(" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) ")" ) "}" )); definitionlet "x", "y" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ); func "x" :::"+"::: "y" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) equals :: ARYTM_2:def 8 "x" if (Bool "y" ($#r1_hidden :::"="::: ) (Set ($#k11_arytm_3 :::"{}"::: ) )) "y" if (Bool "x" ($#r1_hidden :::"="::: ) (Set ($#k11_arytm_3 :::"{}"::: ) )) otherwise (Set ($#k4_arytm_2 :::"GLUED"::: ) (Set "(" (Set "(" ($#k3_arytm_2 :::"DEDEKIND_CUT"::: ) "x" ")" ) ($#k5_arytm_2 :::"+"::: ) (Set "(" ($#k3_arytm_2 :::"DEDEKIND_CUT"::: ) "y" ")" ) ")" )); commutativity (Bool "for" (Set (Var "b1")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) "st" (Bool "(" (Bool (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k11_arytm_3 :::"{}"::: ) ))) "implies" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" & "(" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k11_arytm_3 :::"{}"::: ) ))) "implies" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k11_arytm_3 :::"{}"::: ) ))) & (Bool (Bool "not" (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k11_arytm_3 :::"{}"::: ) )))) "implies" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k4_arytm_2 :::"GLUED"::: ) (Set "(" (Set "(" ($#k3_arytm_2 :::"DEDEKIND_CUT"::: ) (Set (Var "x")) ")" ) ($#k5_arytm_2 :::"+"::: ) (Set "(" ($#k3_arytm_2 :::"DEDEKIND_CUT"::: ) (Set (Var "y")) ")" ) ")" ))) ")" ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k11_arytm_3 :::"{}"::: ) ))) "implies" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" & "(" (Bool (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k11_arytm_3 :::"{}"::: ) ))) "implies" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k11_arytm_3 :::"{}"::: ) ))) & (Bool (Bool "not" (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k11_arytm_3 :::"{}"::: ) )))) "implies" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k4_arytm_2 :::"GLUED"::: ) (Set "(" (Set "(" ($#k3_arytm_2 :::"DEDEKIND_CUT"::: ) (Set (Var "y")) ")" ) ($#k5_arytm_2 :::"+"::: ) (Set "(" ($#k3_arytm_2 :::"DEDEKIND_CUT"::: ) (Set (Var "x")) ")" ) ")" ))) ")" ")" )) ; func "x" :::"*'"::: "y" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) equals :: ARYTM_2:def 9 (Set ($#k4_arytm_2 :::"GLUED"::: ) (Set "(" (Set "(" ($#k3_arytm_2 :::"DEDEKIND_CUT"::: ) "x" ")" ) ($#k6_arytm_2 :::"*'"::: ) (Set "(" ($#k3_arytm_2 :::"DEDEKIND_CUT"::: ) "y" ")" ) ")" )); commutativity (Bool "for" (Set (Var "b1")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) "st" (Bool (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k4_arytm_2 :::"GLUED"::: ) (Set "(" (Set "(" ($#k3_arytm_2 :::"DEDEKIND_CUT"::: ) (Set (Var "x")) ")" ) ($#k6_arytm_2 :::"*'"::: ) (Set "(" ($#k3_arytm_2 :::"DEDEKIND_CUT"::: ) (Set (Var "y")) ")" ) ")" )))) "holds" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k4_arytm_2 :::"GLUED"::: ) (Set "(" (Set "(" ($#k3_arytm_2 :::"DEDEKIND_CUT"::: ) (Set (Var "y")) ")" ) ($#k6_arytm_2 :::"*'"::: ) (Set "(" ($#k3_arytm_2 :::"DEDEKIND_CUT"::: ) (Set (Var "x")) ")" ) ")" )))) ; end; :: deftheorem defines :::"+"::: ARYTM_2:def 8 : (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k11_arytm_3 :::"{}"::: ) ))) "implies" (Bool (Set (Set (Var "x")) ($#k7_arytm_2 :::"+"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" & "(" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k11_arytm_3 :::"{}"::: ) ))) "implies" (Bool (Set (Set (Var "x")) ($#k7_arytm_2 :::"+"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k11_arytm_3 :::"{}"::: ) ))) & (Bool (Bool "not" (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k11_arytm_3 :::"{}"::: ) )))) "implies" (Bool (Set (Set (Var "x")) ($#k7_arytm_2 :::"+"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k4_arytm_2 :::"GLUED"::: ) (Set "(" (Set "(" ($#k3_arytm_2 :::"DEDEKIND_CUT"::: ) (Set (Var "x")) ")" ) ($#k5_arytm_2 :::"+"::: ) (Set "(" ($#k3_arytm_2 :::"DEDEKIND_CUT"::: ) (Set (Var "y")) ")" ) ")" ))) ")" ")" )); :: deftheorem defines :::"*'"::: ARYTM_2:def 9 : (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) "holds" (Bool (Set (Set (Var "x")) ($#k8_arytm_2 :::"*'"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k4_arytm_2 :::"GLUED"::: ) (Set "(" (Set "(" ($#k3_arytm_2 :::"DEDEKIND_CUT"::: ) (Set (Var "x")) ")" ) ($#k6_arytm_2 :::"*'"::: ) (Set "(" ($#k3_arytm_2 :::"DEDEKIND_CUT"::: ) (Set (Var "y")) ")" ) ")" )))); theorem :: ARYTM_2:4 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k11_arytm_3 :::"{}"::: ) ))) "holds" (Bool (Set (Set (Var "x")) ($#k8_arytm_2 :::"*'"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k11_arytm_3 :::"{}"::: ) ))) ; theorem :: ARYTM_2:5 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) "st" (Bool (Bool (Set (Set (Var "x")) ($#k7_arytm_2 :::"+"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k11_arytm_3 :::"{}"::: ) ))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k11_arytm_3 :::"{}"::: ) ))) ; theorem :: ARYTM_2:6 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) "holds" (Bool (Set (Set (Var "x")) ($#k7_arytm_2 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k7_arytm_2 :::"+"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k7_arytm_2 :::"+"::: ) (Set (Var "y")) ")" ) ($#k7_arytm_2 :::"+"::: ) (Set (Var "z"))))) ; theorem :: ARYTM_2:7 (Bool "{" (Set (Var "A")) where A "is" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k5_arytm_3 :::"RAT+"::: ) ) : (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_arytm_3 :::"RAT+"::: ) ) "st" (Bool (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool "(" (Bool "(" "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_arytm_3 :::"RAT+"::: ) ) "st" (Bool (Bool (Set (Var "s")) ($#r3_arytm_3 :::"<='"::: ) (Set (Var "r")))) "holds" (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" ) & (Bool "ex" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_arytm_3 :::"RAT+"::: ) ) "st" (Bool "(" (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "r")) ($#r3_arytm_3 :::"<"::: ) (Set (Var "s"))) ")" )) ")" )) "}" "is" ($#v6_ordinal1 :::"c=-linear"::: ) ) ; theorem :: ARYTM_2:8 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) "st" (Bool (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) "st" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Y")))) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "Y")))) "holds" (Bool (Set (Var "x")) ($#r1_arytm_2 :::"<='"::: ) (Set (Var "y"))) ")" )) "holds" (Bool "ex" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) "st" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "Y")))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_arytm_2 :::"<='"::: ) (Set (Var "z"))) & (Bool (Set (Var "z")) ($#r1_arytm_2 :::"<='"::: ) (Set (Var "y"))) ")" )))) ; theorem :: ARYTM_2:9 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r1_arytm_2 :::"<='"::: ) (Set (Var "y")))) "holds" (Bool "ex" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) "st" (Bool (Set (Set (Var "x")) ($#k7_arytm_2 :::"+"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Var "y"))))) ; theorem :: ARYTM_2:10 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) (Bool "ex" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) "st" (Bool "(" (Bool (Set (Set (Var "x")) ($#k7_arytm_2 :::"+"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Var "y"))) "or" (Bool (Set (Set (Var "y")) ($#k7_arytm_2 :::"+"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" ))) ; theorem :: ARYTM_2:11 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) "st" (Bool (Bool (Set (Set (Var "x")) ($#k7_arytm_2 :::"+"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k7_arytm_2 :::"+"::: ) (Set (Var "z"))))) "holds" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "z")))) ; theorem :: ARYTM_2:12 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) "holds" (Bool (Set (Set (Var "x")) ($#k8_arytm_2 :::"*'"::: ) (Set "(" (Set (Var "y")) ($#k8_arytm_2 :::"*'"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k8_arytm_2 :::"*'"::: ) (Set (Var "y")) ")" ) ($#k8_arytm_2 :::"*'"::: ) (Set (Var "z"))))) ; theorem :: ARYTM_2:13 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) "holds" (Bool (Set (Set (Var "x")) ($#k8_arytm_2 :::"*'"::: ) (Set "(" (Set (Var "y")) ($#k7_arytm_2 :::"+"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k8_arytm_2 :::"*'"::: ) (Set (Var "y")) ")" ) ($#k7_arytm_2 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k8_arytm_2 :::"*'"::: ) (Set (Var "z")) ")" )))) ; theorem :: ARYTM_2:14 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k11_arytm_3 :::"{}"::: ) ))) "holds" (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) "st" (Bool (Set (Set (Var "x")) ($#k8_arytm_2 :::"*'"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k12_arytm_3 :::"one"::: ) )))) ; theorem :: ARYTM_2:15 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k12_arytm_3 :::"one"::: ) ))) "holds" (Bool (Set (Set (Var "x")) ($#k8_arytm_2 :::"*'"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Var "y")))) ; theorem :: ARYTM_2:16 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k4_ordinal1 :::"omega"::: ) )) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k4_ordinal1 :::"omega"::: ) ))) "holds" (Bool (Set (Set (Var "y")) ($#k7_arytm_2 :::"+"::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_ordinal1 :::"omega"::: ) ))) ; theorem :: ARYTM_2:17 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) "st" (Bool (Bool (Set ($#k11_arytm_3 :::"{}"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k12_arytm_3 :::"one"::: ) ))) "holds" (Bool (Set (Set (Var "x")) ($#k7_arytm_2 :::"+"::: ) (Set (Var "y"))) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" )) "holds" (Bool (Set ($#k4_ordinal1 :::"omega"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Var "A")))) ; theorem :: ARYTM_2:18 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k4_ordinal1 :::"omega"::: ) ))) "holds" (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) "holds" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "x"))) "iff" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k4_ordinal1 :::"omega"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) (Set (Var "x"))) & (Bool (Set (Var "y")) ($#r1_arytm_2 :::"<='"::: ) (Set (Var "x"))) ")" ) ")" ))) ; theorem :: ARYTM_2:19 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k7_arytm_2 :::"+"::: ) (Set (Var "z"))))) "holds" (Bool (Set (Var "z")) ($#r1_arytm_2 :::"<='"::: ) (Set (Var "x")))) ; theorem :: ARYTM_2:20 (Bool "(" (Bool (Set ($#k11_arytm_3 :::"{}"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_arytm_2 :::"REAL+"::: ) )) & (Bool (Set ($#k12_arytm_3 :::"one"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_arytm_2 :::"REAL+"::: ) )) ")" ) ; theorem :: ARYTM_2:21 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_arytm_2 :::"REAL+"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k5_arytm_3 :::"RAT+"::: ) )) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k5_arytm_3 :::"RAT+"::: ) ))) "holds" (Bool "ex" (Set (Var "x9")) "," (Set (Var "y9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_arytm_3 :::"RAT+"::: ) ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x9"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "y9"))) & (Bool (Set (Set (Var "x")) ($#k8_arytm_2 :::"*'"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x9")) ($#k10_arytm_3 :::"*'"::: ) (Set (Var "y9")))) ")" ))) ;