:: METRIC_3 semantic presentation begin scheme :: METRIC_3:sch 1 LambdaMCART{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F3() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F4( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F3 "(" ")" ) } : (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set F3 "(" ")" ) "st" (Bool "for" (Set (Var "x1")) "," (Set (Var "y1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "x2")) "," (Set (Var "y2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k1_domain_1 :::"]"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k1_domain_1 :::"]"::: ) ))) "holds" (Bool (Set (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x2")) "," (Set (Var "y2")) ")" )))))) proof end; definitionlet "X", "Y" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::); func :::"dist_cart2"::: "(" "X" "," "Y" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "Y") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "Y") ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: METRIC_3:def 1 (Bool "for" (Set (Var "x1")) "," (Set (Var "y1")) "being" ($#m1_subset_1 :::"Element":::) "of" "X" (Bool "for" (Set (Var "x2")) "," (Set (Var "y2")) "being" ($#m1_subset_1 :::"Element":::) "of" "Y" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "Y") ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k1_domain_1 :::"]"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k1_domain_1 :::"]"::: ) ))) "holds" (Bool (Set it ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) ")" ")" )))))); end; :: deftheorem defines :::"dist_cart2"::: METRIC_3:def 1 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y"))) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y"))) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_metric_3 :::"dist_cart2"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" )) "iff" (Bool "for" (Set (Var "x1")) "," (Set (Var "y1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "x2")) "," (Set (Var "y2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Y")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y"))) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k1_domain_1 :::"]"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k1_domain_1 :::"]"::: ) ))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) ")" ")" )))))) ")" ))); theorem :: METRIC_3:1 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y"))) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k1_metric_3 :::"dist_cart2"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ")" ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "iff" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" ))) ; theorem :: METRIC_3:2 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y"))) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool (Set (Set "(" ($#k1_metric_3 :::"dist_cart2"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ")" ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_metric_3 :::"dist_cart2"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ")" ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "y")) "," (Set (Var "x")) ")" )))) ; theorem :: METRIC_3:3 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y"))) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool (Set (Set "(" ($#k1_metric_3 :::"dist_cart2"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ")" ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "z")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set "(" ($#k1_metric_3 :::"dist_cart2"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ")" ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k1_metric_3 :::"dist_cart2"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ")" ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "y")) "," (Set (Var "z")) ")" ")" ))))) ; definitionlet "X", "Y" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::); let "x", "y" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "X"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "Y"))) ($#k2_zfmisc_1 :::":]"::: ) ); func :::"dist2"::: "(" "x" "," "y" ")" -> ($#m1_subset_1 :::"Real":::) equals :: METRIC_3:def 2 (Set (Set "(" ($#k1_metric_3 :::"dist_cart2"::: ) "(" "X" "," "Y" ")" ")" ) ($#k1_metric_1 :::"."::: ) "(" "x" "," "y" ")" ); end; :: deftheorem defines :::"dist2"::: METRIC_3:def 2 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y"))) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool (Set ($#k2_metric_3 :::"dist2"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_metric_3 :::"dist_cart2"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ")" ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )))); registrationlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "r" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "A")) "," (Set (Const "A")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set ($#g1_metric_1 :::"MetrStruct"::: ) "(#" "A" "," "r" "#)" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ; end; definitionlet "X", "Y" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::); func :::"MetrSpaceCart2"::: "(" "X" "," "Y" ")" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_metric_1 :::"strict"::: ) ($#l1_metric_1 :::"MetrSpace":::) equals :: METRIC_3:def 3 (Set ($#g1_metric_1 :::"MetrStruct"::: ) "(#" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "Y") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k1_metric_3 :::"dist_cart2"::: ) "(" "X" "," "Y" ")" ")" ) "#)" ); end; :: deftheorem defines :::"MetrSpaceCart2"::: METRIC_3:def 3 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) "holds" (Bool (Set ($#k3_metric_3 :::"MetrSpaceCart2"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#g1_metric_1 :::"MetrStruct"::: ) "(#" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y"))) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k1_metric_3 :::"dist_cart2"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ")" ) "#)" ))); scheme :: METRIC_3:sch 2 LambdaMCART1{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F3() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F4() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F5( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F4 "(" ")" ) } : (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) "," (Set F3 "(" ")" ) ($#k3_zfmisc_1 :::":]"::: ) ) "," (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) "," (Set F3 "(" ")" ) ($#k3_zfmisc_1 :::":]"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set F4 "(" ")" ) "st" (Bool "for" (Set (Var "x1")) "," (Set (Var "y1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "x2")) "," (Set (Var "y2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) (Bool "for" (Set (Var "x3")) "," (Set (Var "y3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F3 "(" ")" ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) "," (Set F3 "(" ")" ) ($#k3_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k4_domain_1 :::"]"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) ($#k4_domain_1 :::"]"::: ) ))) "holds" (Bool (Set (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x2")) "," (Set (Var "y2")) "," (Set (Var "x3")) "," (Set (Var "y3")) ")" ))))))) proof end; definitionlet "X", "Y", "Z" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::); func :::"dist_cart3"::: "(" "X" "," "Y" "," "Z" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "Y") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "Z") ($#k3_zfmisc_1 :::":]"::: ) ) "," (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "Y") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "Z") ($#k3_zfmisc_1 :::":]"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: METRIC_3:def 4 (Bool "for" (Set (Var "x1")) "," (Set (Var "y1")) "being" ($#m1_subset_1 :::"Element":::) "of" "X" (Bool "for" (Set (Var "x2")) "," (Set (Var "y2")) "being" ($#m1_subset_1 :::"Element":::) "of" "Y" (Bool "for" (Set (Var "x3")) "," (Set (Var "y3")) "being" ($#m1_subset_1 :::"Element":::) "of" "Z" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "Y") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "Z") ($#k3_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k4_domain_1 :::"]"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) ($#k4_domain_1 :::"]"::: ) ))) "holds" (Bool (Set it ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) ")" ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "x3")) "," (Set (Var "y3")) ")" ")" ))))))); end; :: deftheorem defines :::"dist_cart3"::: METRIC_3:def 4 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Z"))) ($#k3_zfmisc_1 :::":]"::: ) ) "," (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Z"))) ($#k3_zfmisc_1 :::":]"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k4_metric_3 :::"dist_cart3"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) ")" )) "iff" (Bool "for" (Set (Var "x1")) "," (Set (Var "y1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "x2")) "," (Set (Var "y2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Y")) (Bool "for" (Set (Var "x3")) "," (Set (Var "y3")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Z")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Z"))) ($#k3_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k4_domain_1 :::"]"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) ($#k4_domain_1 :::"]"::: ) ))) "holds" (Bool (Set (Set (Var "b4")) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) ")" ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "x3")) "," (Set (Var "y3")) ")" ")" ))))))) ")" ))); theorem :: METRIC_3:4 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Z"))) ($#k3_zfmisc_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k4_metric_3 :::"dist_cart3"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) ")" ")" ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "iff" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" ))) ; theorem :: METRIC_3:5 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Z"))) ($#k3_zfmisc_1 :::":]"::: ) ) "holds" (Bool (Set (Set "(" ($#k4_metric_3 :::"dist_cart3"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) ")" ")" ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_metric_3 :::"dist_cart3"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) ")" ")" ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "y")) "," (Set (Var "x")) ")" )))) ; theorem :: METRIC_3:6 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Z"))) ($#k3_zfmisc_1 :::":]"::: ) ) "holds" (Bool (Set (Set "(" ($#k4_metric_3 :::"dist_cart3"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) ")" ")" ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "z")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set "(" ($#k4_metric_3 :::"dist_cart3"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) ")" ")" ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k4_metric_3 :::"dist_cart3"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) ")" ")" ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "y")) "," (Set (Var "z")) ")" ")" ))))) ; definitionlet "X", "Y", "Z" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::); func :::"MetrSpaceCart3"::: "(" "X" "," "Y" "," "Z" ")" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_metric_1 :::"strict"::: ) ($#l1_metric_1 :::"MetrSpace":::) equals :: METRIC_3:def 5 (Set ($#g1_metric_1 :::"MetrStruct"::: ) "(#" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "Y") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "Z") ($#k3_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k4_metric_3 :::"dist_cart3"::: ) "(" "X" "," "Y" "," "Z" ")" ")" ) "#)" ); end; :: deftheorem defines :::"MetrSpaceCart3"::: METRIC_3:def 5 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) "holds" (Bool (Set ($#k5_metric_3 :::"MetrSpaceCart3"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#g1_metric_1 :::"MetrStruct"::: ) "(#" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Z"))) ($#k3_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k4_metric_3 :::"dist_cart3"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) ")" ")" ) "#)" ))); definitionlet "X", "Y", "Z" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::); let "x", "y" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "X"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "Y"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "Z"))) ($#k3_zfmisc_1 :::":]"::: ) ); func :::"dist3"::: "(" "x" "," "y" ")" -> ($#m1_subset_1 :::"Real":::) equals :: METRIC_3:def 6 (Set (Set "(" ($#k4_metric_3 :::"dist_cart3"::: ) "(" "X" "," "Y" "," "Z" ")" ")" ) ($#k1_metric_1 :::"."::: ) "(" "x" "," "y" ")" ); end; :: deftheorem defines :::"dist3"::: METRIC_3:def 6 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Z"))) ($#k3_zfmisc_1 :::":]"::: ) ) "holds" (Bool (Set ($#k6_metric_3 :::"dist3"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_metric_3 :::"dist_cart3"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) ")" ")" ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )))); scheme :: METRIC_3:sch 3 LambdaMCART2{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F3() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F4() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F5() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F6( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F5 "(" ")" ) } : (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) "," (Set F3 "(" ")" ) "," (Set F4 "(" ")" ) ($#k4_zfmisc_1 :::":]"::: ) ) "," (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) "," (Set F3 "(" ")" ) "," (Set F4 "(" ")" ) ($#k4_zfmisc_1 :::":]"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set F5 "(" ")" ) "st" (Bool "for" (Set (Var "x1")) "," (Set (Var "y1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "x2")) "," (Set (Var "y2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) (Bool "for" (Set (Var "x3")) "," (Set (Var "y3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F3 "(" ")" ) (Bool "for" (Set (Var "x4")) "," (Set (Var "y4")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F4 "(" ")" ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) "," (Set F3 "(" ")" ) "," (Set F4 "(" ")" ) ($#k4_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k5_domain_1 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k5_domain_1 :::"]"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k5_domain_1 :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) "," (Set (Var "y4")) ($#k5_domain_1 :::"]"::: ) ))) "holds" (Bool (Set (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set F6 "(" (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x2")) "," (Set (Var "y2")) "," (Set (Var "x3")) "," (Set (Var "y3")) "," (Set (Var "x4")) "," (Set (Var "y4")) ")" )))))))) proof end; definitionlet "X", "Y", "Z", "W" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::); func :::"dist_cart4"::: "(" "X" "," "Y" "," "Z" "," "W" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "Y") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "Z") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "W") ($#k4_zfmisc_1 :::":]"::: ) ) "," (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "Y") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "Z") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "W") ($#k4_zfmisc_1 :::":]"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: METRIC_3:def 7 (Bool "for" (Set (Var "x1")) "," (Set (Var "y1")) "being" ($#m1_subset_1 :::"Element":::) "of" "X" (Bool "for" (Set (Var "x2")) "," (Set (Var "y2")) "being" ($#m1_subset_1 :::"Element":::) "of" "Y" (Bool "for" (Set (Var "x3")) "," (Set (Var "y3")) "being" ($#m1_subset_1 :::"Element":::) "of" "Z" (Bool "for" (Set (Var "x4")) "," (Set (Var "y4")) "being" ($#m1_subset_1 :::"Element":::) "of" "W" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "Y") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "Z") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "W") ($#k4_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k5_domain_1 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k5_domain_1 :::"]"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k5_domain_1 :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) "," (Set (Var "y4")) ($#k5_domain_1 :::"]"::: ) ))) "holds" (Bool (Set it ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) ")" ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "x3")) "," (Set (Var "y3")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "x4")) "," (Set (Var "y4")) ")" ")" ) ")" )))))))); end; :: deftheorem defines :::"dist_cart4"::: METRIC_3:def 7 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "," (Set (Var "W")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Z"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "W"))) ($#k4_zfmisc_1 :::":]"::: ) ) "," (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Z"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "W"))) ($#k4_zfmisc_1 :::":]"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k7_metric_3 :::"dist_cart4"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "," (Set (Var "W")) ")" )) "iff" (Bool "for" (Set (Var "x1")) "," (Set (Var "y1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "x2")) "," (Set (Var "y2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Y")) (Bool "for" (Set (Var "x3")) "," (Set (Var "y3")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Z")) (Bool "for" (Set (Var "x4")) "," (Set (Var "y4")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "W")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Z"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "W"))) ($#k4_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k5_domain_1 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k5_domain_1 :::"]"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k5_domain_1 :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) "," (Set (Var "y4")) ($#k5_domain_1 :::"]"::: ) ))) "holds" (Bool (Set (Set (Var "b5")) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) ")" ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "x3")) "," (Set (Var "y3")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "x4")) "," (Set (Var "y4")) ")" ")" ) ")" )))))))) ")" ))); theorem :: METRIC_3:7 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "," (Set (Var "W")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Z"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "W"))) ($#k4_zfmisc_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k7_metric_3 :::"dist_cart4"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "," (Set (Var "W")) ")" ")" ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "iff" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" ))) ; theorem :: METRIC_3:8 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "," (Set (Var "W")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Z"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "W"))) ($#k4_zfmisc_1 :::":]"::: ) ) "holds" (Bool (Set (Set "(" ($#k7_metric_3 :::"dist_cart4"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "," (Set (Var "W")) ")" ")" ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_metric_3 :::"dist_cart4"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "," (Set (Var "W")) ")" ")" ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "y")) "," (Set (Var "x")) ")" )))) ; theorem :: METRIC_3:9 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "," (Set (Var "W")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Z"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "W"))) ($#k4_zfmisc_1 :::":]"::: ) ) "holds" (Bool (Set (Set "(" ($#k7_metric_3 :::"dist_cart4"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "," (Set (Var "W")) ")" ")" ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "z")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set "(" ($#k7_metric_3 :::"dist_cart4"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "," (Set (Var "W")) ")" ")" ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k7_metric_3 :::"dist_cart4"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "," (Set (Var "W")) ")" ")" ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "y")) "," (Set (Var "z")) ")" ")" ))))) ; definitionlet "X", "Y", "Z", "W" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::); func :::"MetrSpaceCart4"::: "(" "X" "," "Y" "," "Z" "," "W" ")" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_metric_1 :::"strict"::: ) ($#l1_metric_1 :::"MetrSpace":::) equals :: METRIC_3:def 8 (Set ($#g1_metric_1 :::"MetrStruct"::: ) "(#" (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "Y") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "Z") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "W") ($#k4_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k7_metric_3 :::"dist_cart4"::: ) "(" "X" "," "Y" "," "Z" "," "W" ")" ")" ) "#)" ); end; :: deftheorem defines :::"MetrSpaceCart4"::: METRIC_3:def 8 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "," (Set (Var "W")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) "holds" (Bool (Set ($#k8_metric_3 :::"MetrSpaceCart4"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "," (Set (Var "W")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#g1_metric_1 :::"MetrStruct"::: ) "(#" (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Z"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "W"))) ($#k4_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k7_metric_3 :::"dist_cart4"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "," (Set (Var "W")) ")" ")" ) "#)" ))); definitionlet "X", "Y", "Z", "W" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::); let "x", "y" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "X"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "Y"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "Z"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "W"))) ($#k4_zfmisc_1 :::":]"::: ) ); func :::"dist4"::: "(" "x" "," "y" ")" -> ($#m1_subset_1 :::"Real":::) equals :: METRIC_3:def 9 (Set (Set "(" ($#k7_metric_3 :::"dist_cart4"::: ) "(" "X" "," "Y" "," "Z" "," "W" ")" ")" ) ($#k1_metric_1 :::"."::: ) "(" "x" "," "y" ")" ); end; :: deftheorem defines :::"dist4"::: METRIC_3:def 9 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "," (Set (Var "W")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Z"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "W"))) ($#k4_zfmisc_1 :::":]"::: ) ) "holds" (Bool (Set ($#k9_metric_3 :::"dist4"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_metric_3 :::"dist_cart4"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "," (Set (Var "W")) ")" ")" ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )))); begin definitionlet "X", "Y" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::); func :::"dist_cart2S"::: "(" "X" "," "Y" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "Y") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "Y") ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: METRIC_3:def 10 (Bool "for" (Set (Var "x1")) "," (Set (Var "y1")) "being" ($#m1_subset_1 :::"Element":::) "of" "X" (Bool "for" (Set (Var "x2")) "," (Set (Var "y2")) "being" ($#m1_subset_1 :::"Element":::) "of" "Y" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "Y") ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k1_domain_1 :::"]"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k1_domain_1 :::"]"::: ) ))) "holds" (Bool (Set it ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) ")" ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) ")" ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" )))))); end; :: deftheorem defines :::"dist_cart2S"::: METRIC_3:def 10 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y"))) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y"))) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k10_metric_3 :::"dist_cart2S"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" )) "iff" (Bool "for" (Set (Var "x1")) "," (Set (Var "y1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "x2")) "," (Set (Var "y2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Y")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y"))) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k1_domain_1 :::"]"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k1_domain_1 :::"]"::: ) ))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) ")" ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) ")" ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" )))))) ")" ))); theorem :: METRIC_3:10 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y"))) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k10_metric_3 :::"dist_cart2S"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ")" ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "iff" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" ))) ; theorem :: METRIC_3:11 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y"))) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool (Set (Set "(" ($#k10_metric_3 :::"dist_cart2S"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ")" ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_metric_3 :::"dist_cart2S"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ")" ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "y")) "," (Set (Var "x")) ")" )))) ; theorem :: METRIC_3:12 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "a"))) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b"))) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "c"))) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "d")))) "holds" (Bool (Set ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "c")) ")" ) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Set (Var "b")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "d")) ")" ) ($#k3_square_1 :::"^2"::: ) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "c")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "d")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ")" )))) ; theorem :: METRIC_3:13 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y"))) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool (Set (Set "(" ($#k10_metric_3 :::"dist_cart2S"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ")" ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "z")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set "(" ($#k10_metric_3 :::"dist_cart2S"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ")" ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k10_metric_3 :::"dist_cart2S"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ")" ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "y")) "," (Set (Var "z")) ")" ")" ))))) ; definitionlet "X", "Y" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::); let "x", "y" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "X"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "Y"))) ($#k2_zfmisc_1 :::":]"::: ) ); func :::"dist2S"::: "(" "x" "," "y" ")" -> ($#m1_subset_1 :::"Real":::) equals :: METRIC_3:def 11 (Set (Set "(" ($#k10_metric_3 :::"dist_cart2S"::: ) "(" "X" "," "Y" ")" ")" ) ($#k1_metric_1 :::"."::: ) "(" "x" "," "y" ")" ); end; :: deftheorem defines :::"dist2S"::: METRIC_3:def 11 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y"))) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool (Set ($#k11_metric_3 :::"dist2S"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_metric_3 :::"dist_cart2S"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ")" ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )))); definitionlet "X", "Y" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::); func :::"MetrSpaceCart2S"::: "(" "X" "," "Y" ")" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_metric_1 :::"strict"::: ) ($#l1_metric_1 :::"MetrSpace":::) equals :: METRIC_3:def 12 (Set ($#g1_metric_1 :::"MetrStruct"::: ) "(#" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "Y") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k10_metric_3 :::"dist_cart2S"::: ) "(" "X" "," "Y" ")" ")" ) "#)" ); end; :: deftheorem defines :::"MetrSpaceCart2S"::: METRIC_3:def 12 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) "holds" (Bool (Set ($#k12_metric_3 :::"MetrSpaceCart2S"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#g1_metric_1 :::"MetrStruct"::: ) "(#" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y"))) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k10_metric_3 :::"dist_cart2S"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ")" ) "#)" ))); begin definitionlet "X", "Y", "Z" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::); func :::"dist_cart3S"::: "(" "X" "," "Y" "," "Z" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "Y") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "Z") ($#k3_zfmisc_1 :::":]"::: ) ) "," (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "Y") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "Z") ($#k3_zfmisc_1 :::":]"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: METRIC_3:def 13 (Bool "for" (Set (Var "x1")) "," (Set (Var "y1")) "being" ($#m1_subset_1 :::"Element":::) "of" "X" (Bool "for" (Set (Var "x2")) "," (Set (Var "y2")) "being" ($#m1_subset_1 :::"Element":::) "of" "Y" (Bool "for" (Set (Var "x3")) "," (Set (Var "y3")) "being" ($#m1_subset_1 :::"Element":::) "of" "Z" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "Y") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "Z") ($#k3_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k4_domain_1 :::"]"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) ($#k4_domain_1 :::"]"::: ) ))) "holds" (Bool (Set it ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set "(" ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) ")" ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) ")" ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "x3")) "," (Set (Var "y3")) ")" ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ))))))); end; :: deftheorem defines :::"dist_cart3S"::: METRIC_3:def 13 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Z"))) ($#k3_zfmisc_1 :::":]"::: ) ) "," (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Z"))) ($#k3_zfmisc_1 :::":]"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k13_metric_3 :::"dist_cart3S"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) ")" )) "iff" (Bool "for" (Set (Var "x1")) "," (Set (Var "y1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "x2")) "," (Set (Var "y2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Y")) (Bool "for" (Set (Var "x3")) "," (Set (Var "y3")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Z")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Z"))) ($#k3_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k4_domain_1 :::"]"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) ($#k4_domain_1 :::"]"::: ) ))) "holds" (Bool (Set (Set (Var "b4")) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set "(" ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) ")" ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) ")" ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "x3")) "," (Set (Var "y3")) ")" ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ))))))) ")" ))); theorem :: METRIC_3:14 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Z"))) ($#k3_zfmisc_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k13_metric_3 :::"dist_cart3S"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) ")" ")" ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "iff" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" ))) ; theorem :: METRIC_3:15 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Z"))) ($#k3_zfmisc_1 :::":]"::: ) ) "holds" (Bool (Set (Set "(" ($#k13_metric_3 :::"dist_cart3S"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) ")" ")" ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k13_metric_3 :::"dist_cart3S"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) ")" ")" ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "y")) "," (Set (Var "x")) ")" )))) ; theorem :: METRIC_3:16 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "d")) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "c")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "b")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "f")) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "e")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "c")) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "f")) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "e")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "d")) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "d")) ")" ) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Set (Var "c")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "b")) ")" ) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "f")) ")" ) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Set (Var "e")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "c")) ")" ) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Set (Var "b")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "f")) ")" ) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Set (Var "e")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "d")) ")" ) ($#k3_square_1 :::"^2"::: ) ")" )))) ; theorem :: METRIC_3:17 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "c")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "d")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "e")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "f")) ")" ) ")" ) ($#k3_square_1 :::"^2"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "e")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "c")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "d")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "f")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" )))) ; theorem :: METRIC_3:18 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Z"))) ($#k3_zfmisc_1 :::":]"::: ) ) "holds" (Bool (Set (Set "(" ($#k13_metric_3 :::"dist_cart3S"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) ")" ")" ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "z")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set "(" ($#k13_metric_3 :::"dist_cart3S"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) ")" ")" ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k13_metric_3 :::"dist_cart3S"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) ")" ")" ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "y")) "," (Set (Var "z")) ")" ")" ))))) ; definitionlet "X", "Y", "Z" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::); let "x", "y" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "X"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "Y"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "Z"))) ($#k3_zfmisc_1 :::":]"::: ) ); func :::"dist3S"::: "(" "x" "," "y" ")" -> ($#m1_subset_1 :::"Real":::) equals :: METRIC_3:def 14 (Set (Set "(" ($#k13_metric_3 :::"dist_cart3S"::: ) "(" "X" "," "Y" "," "Z" ")" ")" ) ($#k1_metric_1 :::"."::: ) "(" "x" "," "y" ")" ); end; :: deftheorem defines :::"dist3S"::: METRIC_3:def 14 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Z"))) ($#k3_zfmisc_1 :::":]"::: ) ) "holds" (Bool (Set ($#k14_metric_3 :::"dist3S"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k13_metric_3 :::"dist_cart3S"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) ")" ")" ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )))); definitionlet "X", "Y", "Z" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::); func :::"MetrSpaceCart3S"::: "(" "X" "," "Y" "," "Z" ")" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_metric_1 :::"strict"::: ) ($#l1_metric_1 :::"MetrSpace":::) equals :: METRIC_3:def 15 (Set ($#g1_metric_1 :::"MetrStruct"::: ) "(#" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "Y") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "Z") ($#k3_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k13_metric_3 :::"dist_cart3S"::: ) "(" "X" "," "Y" "," "Z" ")" ")" ) "#)" ); end; :: deftheorem defines :::"MetrSpaceCart3S"::: METRIC_3:def 15 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) "holds" (Bool (Set ($#k15_metric_3 :::"MetrSpaceCart3S"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#g1_metric_1 :::"MetrStruct"::: ) "(#" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Z"))) ($#k3_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k13_metric_3 :::"dist_cart3S"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) ")" ")" ) "#)" ))); definitionfunc :::"taxi_dist2"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: METRIC_3:def 16 (Bool "for" (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x2")) "," (Set (Var "y2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k1_domain_1 :::"]"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k1_domain_1 :::"]"::: ) ))) "holds" (Bool (Set it ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k7_metric_1 :::"real_dist"::: ) ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set ($#k7_metric_1 :::"real_dist"::: ) ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) ")" ")" ))))); end; :: deftheorem defines :::"taxi_dist2"::: METRIC_3:def 16 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k16_metric_3 :::"taxi_dist2"::: ) )) "iff" (Bool "for" (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x2")) "," (Set (Var "y2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k1_domain_1 :::"]"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k1_domain_1 :::"]"::: ) ))) "holds" (Bool (Set (Set (Var "b1")) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k7_metric_1 :::"real_dist"::: ) ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set ($#k7_metric_1 :::"real_dist"::: ) ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) ")" ")" ))))) ")" )); theorem :: METRIC_3:19 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Set ($#k16_metric_3 :::"taxi_dist2"::: ) ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "iff" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" )) ; theorem :: METRIC_3:20 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool (Set (Set ($#k16_metric_3 :::"taxi_dist2"::: ) ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k16_metric_3 :::"taxi_dist2"::: ) ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "y")) "," (Set (Var "x")) ")" ))) ; theorem :: METRIC_3:21 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool (Set (Set ($#k16_metric_3 :::"taxi_dist2"::: ) ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "z")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set ($#k16_metric_3 :::"taxi_dist2"::: ) ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set ($#k16_metric_3 :::"taxi_dist2"::: ) ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "y")) "," (Set (Var "z")) ")" ")" )))) ; definitionfunc :::"RealSpaceCart2"::: -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_metric_1 :::"strict"::: ) ($#l1_metric_1 :::"MetrSpace":::) equals :: METRIC_3:def 17 (Set ($#g1_metric_1 :::"MetrStruct"::: ) "(#" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k16_metric_3 :::"taxi_dist2"::: ) ) "#)" ); end; :: deftheorem defines :::"RealSpaceCart2"::: METRIC_3:def 17 : (Bool (Set ($#k17_metric_3 :::"RealSpaceCart2"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#g1_metric_1 :::"MetrStruct"::: ) "(#" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k16_metric_3 :::"taxi_dist2"::: ) ) "#)" )); definitionfunc :::"Eukl_dist2"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: METRIC_3:def 18 (Bool "for" (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x2")) "," (Set (Var "y2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k1_domain_1 :::"]"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k1_domain_1 :::"]"::: ) ))) "holds" (Bool (Set it ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set ($#k7_metric_1 :::"real_dist"::: ) ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) ")" ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set ($#k7_metric_1 :::"real_dist"::: ) ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) ")" ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ))))); end; :: deftheorem defines :::"Eukl_dist2"::: METRIC_3:def 18 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k18_metric_3 :::"Eukl_dist2"::: ) )) "iff" (Bool "for" (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x2")) "," (Set (Var "y2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k1_domain_1 :::"]"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k1_domain_1 :::"]"::: ) ))) "holds" (Bool (Set (Set (Var "b1")) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set ($#k7_metric_1 :::"real_dist"::: ) ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) ")" ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set ($#k7_metric_1 :::"real_dist"::: ) ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) ")" ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ))))) ")" )); theorem :: METRIC_3:22 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Set ($#k18_metric_3 :::"Eukl_dist2"::: ) ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "iff" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" )) ; theorem :: METRIC_3:23 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool (Set (Set ($#k18_metric_3 :::"Eukl_dist2"::: ) ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k18_metric_3 :::"Eukl_dist2"::: ) ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "y")) "," (Set (Var "x")) ")" ))) ; theorem :: METRIC_3:24 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool (Set (Set ($#k18_metric_3 :::"Eukl_dist2"::: ) ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "z")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set ($#k18_metric_3 :::"Eukl_dist2"::: ) ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set ($#k18_metric_3 :::"Eukl_dist2"::: ) ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "y")) "," (Set (Var "z")) ")" ")" )))) ; definitionfunc :::"EuklSpace2"::: -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_metric_1 :::"strict"::: ) ($#l1_metric_1 :::"MetrSpace":::) equals :: METRIC_3:def 19 (Set ($#g1_metric_1 :::"MetrStruct"::: ) "(#" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k18_metric_3 :::"Eukl_dist2"::: ) ) "#)" ); end; :: deftheorem defines :::"EuklSpace2"::: METRIC_3:def 19 : (Bool (Set ($#k19_metric_3 :::"EuklSpace2"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#g1_metric_1 :::"MetrStruct"::: ) "(#" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k18_metric_3 :::"Eukl_dist2"::: ) ) "#)" )); definitionfunc :::"taxi_dist3"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_zfmisc_1 :::":]"::: ) ) "," (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_zfmisc_1 :::":]"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: METRIC_3:def 20 (Bool "for" (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x2")) "," (Set (Var "y2")) "," (Set (Var "x3")) "," (Set (Var "y3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k4_domain_1 :::"]"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) ($#k4_domain_1 :::"]"::: ) ))) "holds" (Bool (Set it ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k7_metric_1 :::"real_dist"::: ) ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set ($#k7_metric_1 :::"real_dist"::: ) ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) ")" ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set ($#k7_metric_1 :::"real_dist"::: ) ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x3")) "," (Set (Var "y3")) ")" ")" ))))); end; :: deftheorem defines :::"taxi_dist3"::: METRIC_3:def 20 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_zfmisc_1 :::":]"::: ) ) "," (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_zfmisc_1 :::":]"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k20_metric_3 :::"taxi_dist3"::: ) )) "iff" (Bool "for" (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x2")) "," (Set (Var "y2")) "," (Set (Var "x3")) "," (Set (Var "y3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k4_domain_1 :::"]"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) ($#k4_domain_1 :::"]"::: ) ))) "holds" (Bool (Set (Set (Var "b1")) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k7_metric_1 :::"real_dist"::: ) ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set ($#k7_metric_1 :::"real_dist"::: ) ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) ")" ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set ($#k7_metric_1 :::"real_dist"::: ) ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x3")) "," (Set (Var "y3")) ")" ")" ))))) ")" )); theorem :: METRIC_3:25 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_zfmisc_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Set ($#k20_metric_3 :::"taxi_dist3"::: ) ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "iff" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" )) ; theorem :: METRIC_3:26 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_zfmisc_1 :::":]"::: ) ) "holds" (Bool (Set (Set ($#k20_metric_3 :::"taxi_dist3"::: ) ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k20_metric_3 :::"taxi_dist3"::: ) ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "y")) "," (Set (Var "x")) ")" ))) ; theorem :: METRIC_3:27 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_zfmisc_1 :::":]"::: ) ) "holds" (Bool (Set (Set ($#k20_metric_3 :::"taxi_dist3"::: ) ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "z")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set ($#k20_metric_3 :::"taxi_dist3"::: ) ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set ($#k20_metric_3 :::"taxi_dist3"::: ) ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "y")) "," (Set (Var "z")) ")" ")" )))) ; definitionfunc :::"RealSpaceCart3"::: -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_metric_1 :::"strict"::: ) ($#l1_metric_1 :::"MetrSpace":::) equals :: METRIC_3:def 21 (Set ($#g1_metric_1 :::"MetrStruct"::: ) "(#" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_zfmisc_1 :::":]"::: ) ) "," (Set ($#k20_metric_3 :::"taxi_dist3"::: ) ) "#)" ); end; :: deftheorem defines :::"RealSpaceCart3"::: METRIC_3:def 21 : (Bool (Set ($#k21_metric_3 :::"RealSpaceCart3"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#g1_metric_1 :::"MetrStruct"::: ) "(#" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_zfmisc_1 :::":]"::: ) ) "," (Set ($#k20_metric_3 :::"taxi_dist3"::: ) ) "#)" )); definitionfunc :::"Eukl_dist3"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_zfmisc_1 :::":]"::: ) ) "," (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_zfmisc_1 :::":]"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: METRIC_3:def 22 (Bool "for" (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x2")) "," (Set (Var "y2")) "," (Set (Var "x3")) "," (Set (Var "y3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k4_domain_1 :::"]"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) ($#k4_domain_1 :::"]"::: ) ))) "holds" (Bool (Set it ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set ($#k7_metric_1 :::"real_dist"::: ) ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) ")" ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set ($#k7_metric_1 :::"real_dist"::: ) ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) ")" ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set ($#k7_metric_1 :::"real_dist"::: ) ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x3")) "," (Set (Var "y3")) ")" ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ))))); end; :: deftheorem defines :::"Eukl_dist3"::: METRIC_3:def 22 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_zfmisc_1 :::":]"::: ) ) "," (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_zfmisc_1 :::":]"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k22_metric_3 :::"Eukl_dist3"::: ) )) "iff" (Bool "for" (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x2")) "," (Set (Var "y2")) "," (Set (Var "x3")) "," (Set (Var "y3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k4_domain_1 :::"]"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) ($#k4_domain_1 :::"]"::: ) ))) "holds" (Bool (Set (Set (Var "b1")) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set ($#k7_metric_1 :::"real_dist"::: ) ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) ")" ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set ($#k7_metric_1 :::"real_dist"::: ) ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) ")" ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set ($#k7_metric_1 :::"real_dist"::: ) ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x3")) "," (Set (Var "y3")) ")" ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ))))) ")" )); theorem :: METRIC_3:28 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_zfmisc_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Set ($#k22_metric_3 :::"Eukl_dist3"::: ) ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "iff" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" )) ; theorem :: METRIC_3:29 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_zfmisc_1 :::":]"::: ) ) "holds" (Bool (Set (Set ($#k22_metric_3 :::"Eukl_dist3"::: ) ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k22_metric_3 :::"Eukl_dist3"::: ) ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "y")) "," (Set (Var "x")) ")" ))) ; theorem :: METRIC_3:30 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_zfmisc_1 :::":]"::: ) ) "holds" (Bool (Set (Set ($#k22_metric_3 :::"Eukl_dist3"::: ) ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "z")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set ($#k22_metric_3 :::"Eukl_dist3"::: ) ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set ($#k22_metric_3 :::"Eukl_dist3"::: ) ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "y")) "," (Set (Var "z")) ")" ")" )))) ; definitionfunc :::"EuklSpace3"::: -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_metric_1 :::"strict"::: ) ($#l1_metric_1 :::"MetrSpace":::) equals :: METRIC_3:def 23 (Set ($#g1_metric_1 :::"MetrStruct"::: ) "(#" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_zfmisc_1 :::":]"::: ) ) "," (Set ($#k22_metric_3 :::"Eukl_dist3"::: ) ) "#)" ); end; :: deftheorem defines :::"EuklSpace3"::: METRIC_3:def 23 : (Bool (Set ($#k23_metric_3 :::"EuklSpace3"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#g1_metric_1 :::"MetrStruct"::: ) "(#" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_zfmisc_1 :::":]"::: ) ) "," (Set ($#k22_metric_3 :::"Eukl_dist3"::: ) ) "#)" ));