:: TOLER_1  semantic presentation begin  







registration
cluster   ($#v1_relat_1 :::"Relation-like"::: )     ($#v1_xboole_0 :::"empty"::: )    ->   ($#v1_relat_2 :::"reflexive"::: )     ($#v2_relat_2 :::"irreflexive"::: )     ($#v3_relat_2 :::"symmetric"::: )     ($#v4_relat_2 :::"antisymmetric"::: )     ($#v5_relat_2 :::"asymmetric"::: )     ($#v6_relat_2 :::"connected"::: )     ($#v7_relat_2 :::"strongly_connected"::: )     ($#v8_relat_2 :::"transitive"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; notationlet "X" be    ($#m1_hidden :::"set"::: )  ; synonym  :::"Total"::: "X" for  :::"nabla"::: "X"; end; definitionlet "R" be   ($#m1_hidden :::"Relation":::); let "Y" be    ($#m1_hidden :::"set"::: )  ; :: original: :::"|_2"::: redefine func "R" :::"|_2"::: "Y" ->   ($#m1_subset_1 :::"Relation":::) "of" "Y" "," "Y"; end; 
theorem :: TOLER_1:1 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set  "("  ($#k1_eqrel_1 :::"Total"::: )  (Set (Var "X")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "X")))) ; 
 
theorem :: TOLER_1:2 (Bool  "for" (Set (Var "X")) "," (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k1_eqrel_1 :::"Total"::: )  (Set (Var "X"))))) ; 
 
theorem :: TOLER_1:3 (Bool  "for" (Set (Var "X")) "," (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relat_1 :::"field"::: )  (Set  "("  ($#k1_eqrel_1 :::"Total"::: )  (Set (Var "X")) ")" ))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relat_1 :::"field"::: )  (Set  "("  ($#k1_eqrel_1 :::"Total"::: )  (Set (Var "X")) ")" )))) "holds"  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k1_eqrel_1 :::"Total"::: )  (Set (Var "X"))))) ; 
 
theorem :: TOLER_1:4 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k1_eqrel_1 :::"Total"::: )  (Set (Var "X"))) "is"   ($#v7_relat_2 :::"strongly_connected"::: )  )) ; 
 
theorem :: TOLER_1:5 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k1_eqrel_1 :::"Total"::: )  (Set (Var "X"))) "is"   ($#v6_relat_2 :::"connected"::: )  )) ; 
 




theorem :: TOLER_1:6 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"Tolerance":::) "of" (Set (Var "X")) "holds"  (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "T")))  ($#r1_hidden :::"="::: )  (Set (Var "X"))))) ; 
 
theorem :: TOLER_1:7 (Bool  "for" (Set (Var "X")) "," (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "T")) "being"   ($#v1_relat_2 :::"reflexive"::: )     ($#v1_partfun1 :::"total"::: )    ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X")) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) "iff" (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "T")))  ")" ))) ; 
 
theorem :: TOLER_1:8 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"Tolerance":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Var "T"))  ($#r1_relat_2 :::"is_reflexive_in"::: )  (Set (Var "X"))))) ; 
 
theorem :: TOLER_1:9 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"Tolerance":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Var "T"))  ($#r3_relat_2 :::"is_symmetric_in"::: )  (Set (Var "X"))))) ; 
 
theorem :: TOLER_1:10 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "R")) "being"   ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X")) "," (Set (Var "Y"))  "st" (Bool (Bool (Set (Var "R")) "is"   ($#v3_relat_2 :::"symmetric"::: )  )) "holds"  (Bool (Set (Set (Var "R"))  ($#k1_toler_1 :::"|_2"::: )  (Set (Var "Z"))) "is"   ($#v3_relat_2 :::"symmetric"::: )  ))) ; 
 definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; let "T" be   ($#m1_subset_1 :::"Tolerance":::) "of" (Set (Const "X")); let "Y" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); :: original: :::"|_2"::: redefine func "T" :::"|_2"::: "Y" ->   ($#m1_subset_1 :::"Tolerance":::) "of" "Y"; end; 
theorem :: TOLER_1:11 (Bool  "for" (Set (Var "Y")) "," (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"Tolerance":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "Y"))  ($#r1_tarski :::"c="::: )  (Set (Var "X")))) "holds"  (Bool (Set (Set (Var "T"))  ($#k1_toler_1 :::"|_2"::: )  (Set (Var "Y"))) "is"   ($#m1_subset_1 :::"Tolerance":::) "of" (Set (Var "Y"))))) ; 
 definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; let "T" be   ($#m1_subset_1 :::"Tolerance":::) "of" (Set (Const "X")); mode  :::"TolSet":::  "of" "T" ->    ($#m1_hidden :::"set"::: )   means :: TOLER_1:def 1 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  it) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  it)) "holds"  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  "T")); end; 






:: deftheorem    defines :::"TolSet"::: TOLER_1:def 1 :  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"Tolerance":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "b3")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b3")) "is"    ($#m1_toler_1 :::"TolSet"::: )   "of" (Set (Var "T"))) "iff" (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "b3"))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "b3")))) "holds"  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "T"))))  ")" )))); 
 
theorem :: TOLER_1:12 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"Tolerance":::) "of" (Set (Var "X")) "holds"  (Bool (Set   ($#k1_xboole_0 :::"{}"::: )  ) "is"    ($#m1_toler_1 :::"TolSet"::: )   "of" (Set (Var "T"))))) ; 
 definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; let "T" be   ($#m1_subset_1 :::"Tolerance":::) "of" (Set (Const "X")); let "IT" be    ($#m1_toler_1 :::"TolSet"::: )   "of" (Set (Const "T")); attr "IT" is  :::"TolClass-like":::  means :: TOLER_1:def 2 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Bool  "not" (Set (Var "x"))  ($#r2_hidden :::"in"::: )  "IT")) & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  "X")) "holds"  (Bool  "ex" (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  "IT") & (Bool (Bool  "not" (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  "T"))  ")" ))); end; 






:: deftheorem    defines :::"TolClass-like"::: TOLER_1:def 2 :  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"Tolerance":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "IT")) "being"    ($#m1_toler_1 :::"TolSet"::: )   "of" (Set (Var "T")) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v1_toler_1 :::"TolClass-like"::: )  ) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Bool  "not" (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "IT")))) & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool  "ex" (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "IT"))) & (Bool (Bool  "not" (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "T"))))  ")" )))  ")" )))); 
 registrationlet "X" be    ($#m1_hidden :::"set"::: )  ; let "T" be   ($#m1_subset_1 :::"Tolerance":::) "of" (Set (Const "X")); 
cluster   ($#v1_toler_1 :::"TolClass-like"::: )    for    ($#m1_toler_1 :::"TolSet"::: )   "of" "T"; 
end; definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; let "T" be   ($#m1_subset_1 :::"Tolerance":::) "of" (Set (Const "X")); mode TolClass of "T" is   ($#v1_toler_1 :::"TolClass-like"::: )     ($#m1_toler_1 :::"TolSet"::: )   "of" "T"; end; 
theorem :: TOLER_1:13 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"Tolerance":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set   ($#k1_xboole_0 :::"{}"::: )  ) "is"   ($#m1_toler_1 :::"TolClass":::) "of" (Set (Var "T")))) "holds"  (Bool (Set (Var "T"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )))) ; 
 
theorem :: TOLER_1:14 (Bool (Set   ($#k1_xboole_0 :::"{}"::: )  ) "is"   ($#m1_subset_1 :::"Tolerance":::) "of" (Set  ($#k1_xboole_0 :::"{}"::: ) )) ; 
 
theorem :: TOLER_1:15 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"Tolerance":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "T")))) "holds"  (Bool (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) ) "is"    ($#m1_toler_1 :::"TolSet"::: )   "of" (Set (Var "T")))))) ; 
 
theorem :: TOLER_1:16 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"Tolerance":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) "is"    ($#m1_toler_1 :::"TolSet"::: )   "of" (Set (Var "T")))))) ; 
 
theorem :: TOLER_1:17 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"Tolerance":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "Y")) "," (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "Y")) "is"    ($#m1_toler_1 :::"TolSet"::: )   "of" (Set (Var "T")))) "holds"  (Bool (Set (Set (Var "Y"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Z"))) "is"    ($#m1_toler_1 :::"TolSet"::: )   "of" (Set (Var "T")))))) ; 
 
theorem :: TOLER_1:18 (Bool  "for" (Set (Var "Y")) "," (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"Tolerance":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "Y")) "is"    ($#m1_toler_1 :::"TolSet"::: )   "of" (Set (Var "T")))) "holds"  (Bool (Set (Var "Y"))  ($#r1_tarski :::"c="::: )  (Set (Var "X"))))) ; 
 
theorem :: TOLER_1:19 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"Tolerance":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "Y")) "being"    ($#m1_toler_1 :::"TolSet"::: )   "of" (Set (Var "T")) (Bool  "ex" (Set (Var "Z")) "being"   ($#m1_toler_1 :::"TolClass":::) "of" (Set (Var "T")) "st" (Bool (Set (Var "Y"))  ($#r1_tarski :::"c="::: )  (Set (Var "Z"))))))) ; 
 
theorem :: TOLER_1:20 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"Tolerance":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "T")))) "holds"  (Bool  "ex" (Set (Var "Z")) "being"   ($#m1_toler_1 :::"TolClass":::) "of" (Set (Var "T")) "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z"))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))  ")" ))))) ; 
 
theorem :: TOLER_1:21 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"Tolerance":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool  "ex" (Set (Var "Z")) "being"   ($#m1_toler_1 :::"TolClass":::) "of" (Set (Var "T")) "st" (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z"))))))) ; 
 
theorem :: TOLER_1:22 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"Tolerance":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Var "T"))  ($#r1_relset_1 :::"c="::: )  (Set   ($#k1_eqrel_1 :::"Total"::: )  (Set (Var "X")))))) ; 
 
theorem :: TOLER_1:23 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"Tolerance":::) "of" (Set (Var "X")) "holds"  (Bool (Set   ($#k6_partfun1 :::"id"::: )  (Set (Var "X")))  ($#r1_relset_1 :::"c="::: )  (Set (Var "T"))))) ; 
 scheme  :: TOLER_1:sch 1 ToleranceEx{ F1() ->    ($#m1_hidden :::"set"::: )  , P1[   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "ex" (Set (Var "T")) "being"   ($#m1_subset_1 :::"Tolerance":::) "of" (Set F1 "("  ")" ) "st"  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set F1 "("  ")" )) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set F1 "("  ")" ))) "holds"  (Bool  "("  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "T"))) "iff" (Bool P1[(Set (Var "x")) "," (Set (Var "y"))])  ")" )))
 provided
(Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set F1 "("  ")" ))) "holds"  (Bool P1[(Set (Var "x")) "," (Set (Var "x"))]))
 and  
(Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set F1 "("  ")" )) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set F1 "("  ")" )) & (Bool P1[(Set (Var "x")) "," (Set (Var "y"))])) "holds"  (Bool P1[(Set (Var "y")) "," (Set (Var "x"))]))
 proof 


end; 
theorem :: TOLER_1:24 (Bool  "for" (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   (Bool  "ex" (Set (Var "T")) "being"   ($#m1_subset_1 :::"Tolerance":::) "of" (Set  "("  ($#k3_tarski :::"union"::: )  (Set (Var "Y")) ")" ) "st"  (Bool  "for" (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "Z"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y")))) "holds"  (Bool (Set (Var "Z")) "is"    ($#m1_toler_1 :::"TolSet"::: )   "of" (Set (Var "T")))))) ; 
 
theorem :: TOLER_1:25 (Bool  "for" (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "T")) "," (Set (Var "R")) "being"   ($#m1_subset_1 :::"Tolerance":::) "of" (Set  "("  ($#k3_tarski :::"union"::: )  (Set (Var "Y")) ")" )  "st" (Bool (Bool  "("   "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "T"))) "iff" (Bool  "ex" (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "Z"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y"))) & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z"))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))  ")" ))  ")" )  ")" ) & (Bool  "("   "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "R"))) "iff" (Bool  "ex" (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "Z"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y"))) & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z"))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))  ")" ))  ")" )  ")" )) "holds"  (Bool (Set (Var "T"))  ($#r2_relset_1 :::"="::: )  (Set (Var "R"))))) ; 
 
theorem :: TOLER_1:26 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "T")) "," (Set (Var "R")) "being"   ($#m1_subset_1 :::"Tolerance":::) "of" (Set (Var "X"))  "st" (Bool (Bool  "("   "for" (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "Z")) "is"   ($#m1_toler_1 :::"TolClass":::) "of" (Set (Var "T"))) "iff" (Bool (Set (Var "Z")) "is"   ($#m1_toler_1 :::"TolClass":::) "of" (Set (Var "R")))  ")" )  ")" )) "holds"  (Bool (Set (Var "T"))  ($#r2_relset_1 :::"="::: )  (Set (Var "R"))))) ; 
 notationlet "X", "Y" be    ($#m1_hidden :::"set"::: )  ; let "T" be   ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "X")) "," (Set (Const "Y")); let "x" be    ($#m1_hidden :::"set"::: )  ; synonym  :::"neighbourhood":::  "(" "x" "," "T" ")"  for  :::"Class":::  "(" "X" "," "Y" ")" ; end; 
theorem :: TOLER_1:27 (Bool  "for" (Set (Var "X")) "," (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"Tolerance":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_relat_1 :::"neighbourhood"::: )   "("  ","  ")" )) "iff" (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "T")))  ")" )))) ; 
 
theorem :: TOLER_1:28 (Bool  "for" (Set (Var "X")) "," (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"Tolerance":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool  "("   "for" (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "Z"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y"))) "iff" (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z"))) & (Bool (Set (Var "Z")) "is"   ($#m1_toler_1 :::"TolClass":::) "of" (Set (Var "T")))  ")" )  ")" )  ")" )) "holds"  (Bool (Set   ($#k9_relat_1 :::"neighbourhood"::: )   "("  ","  ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k3_tarski :::"union"::: )  (Set (Var "Y"))))))) ; 
 
theorem :: TOLER_1:29 (Bool  "for" (Set (Var "X")) "," (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"Tolerance":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool  "("   "for" (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "Z"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y"))) "iff" (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z"))) & (Bool (Set (Var "Z")) "is"    ($#m1_toler_1 :::"TolSet"::: )   "of" (Set (Var "T")))  ")" )  ")" )  ")" )) "holds"  (Bool (Set   ($#k9_relat_1 :::"neighbourhood"::: )   "("  ","  ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k3_tarski :::"union"::: )  (Set (Var "Y"))))))) ; 
 definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; let "T" be   ($#m1_subset_1 :::"Tolerance":::) "of" (Set (Const "X")); func  :::"TolSets"::: "T" ->    ($#m1_hidden :::"set"::: )   means :: TOLER_1:def 3 (Bool  "for" (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "Y"))  ($#r2_hidden :::"in"::: )  it) "iff" (Bool (Set (Var "Y")) "is"    ($#m1_toler_1 :::"TolSet"::: )   "of" "T")  ")" )); func  :::"TolClasses"::: "T" ->    ($#m1_hidden :::"set"::: )   means :: TOLER_1:def 4 (Bool  "for" (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "Y"))  ($#r2_hidden :::"in"::: )  it) "iff" (Bool (Set (Var "Y")) "is"   ($#m1_toler_1 :::"TolClass":::) "of" "T")  ")" )); end; 












:: deftheorem    defines :::"TolSets"::: TOLER_1:def 3 :  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"Tolerance":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "b3")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_toler_1 :::"TolSets"::: )  (Set (Var "T")))) "iff" (Bool  "for" (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "Y"))  ($#r2_hidden :::"in"::: )  (Set (Var "b3"))) "iff" (Bool (Set (Var "Y")) "is"    ($#m1_toler_1 :::"TolSet"::: )   "of" (Set (Var "T")))  ")" ))  ")" )))); 
 
:: deftheorem    defines :::"TolClasses"::: TOLER_1:def 4 :  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"Tolerance":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "b3")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_toler_1 :::"TolClasses"::: )  (Set (Var "T")))) "iff" (Bool  "for" (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "Y"))  ($#r2_hidden :::"in"::: )  (Set (Var "b3"))) "iff" (Bool (Set (Var "Y")) "is"   ($#m1_toler_1 :::"TolClass":::) "of" (Set (Var "T")))  ")" ))  ")" )))); 
 
theorem :: TOLER_1:30 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "R")) "," (Set (Var "T")) "being"   ($#m1_subset_1 :::"Tolerance":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set   ($#k4_toler_1 :::"TolClasses"::: )  (Set (Var "R")))  ($#r1_tarski :::"c="::: )  (Set   ($#k4_toler_1 :::"TolClasses"::: )  (Set (Var "T"))))) "holds"  (Bool (Set (Var "R"))  ($#r1_relset_1 :::"c="::: )  (Set (Var "T"))))) ; 
 
theorem :: TOLER_1:31 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "T")) "," (Set (Var "R")) "being"   ($#m1_subset_1 :::"Tolerance":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set   ($#k4_toler_1 :::"TolClasses"::: )  (Set (Var "T")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_toler_1 :::"TolClasses"::: )  (Set (Var "R"))))) "holds"  (Bool (Set (Var "T"))  ($#r2_relset_1 :::"="::: )  (Set (Var "R"))))) ; 
 
theorem :: TOLER_1:32 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"Tolerance":::) "of" (Set (Var "X")) "holds"  (Bool (Set   ($#k3_tarski :::"union"::: )  (Set  "("  ($#k4_toler_1 :::"TolClasses"::: )  (Set (Var "T")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "X"))))) ; 
 
theorem :: TOLER_1:33 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"Tolerance":::) "of" (Set (Var "X")) "holds"  (Bool (Set   ($#k3_tarski :::"union"::: )  (Set  "("  ($#k3_toler_1 :::"TolSets"::: )  (Set (Var "T")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "X"))))) ; 
 
theorem :: TOLER_1:34 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"Tolerance":::) "of" (Set (Var "X"))  "st" (Bool (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set   ($#k9_relat_1 :::"neighbourhood"::: )   "("  ","  ")" ) "is"    ($#m1_toler_1 :::"TolSet"::: )   "of" (Set (Var "T")))  ")" )) "holds"  (Bool (Set (Var "T")) "is"   ($#v8_relat_2 :::"transitive"::: )  ))) ; 
 
theorem :: TOLER_1:35 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"Tolerance":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "T")) "is"   ($#v8_relat_2 :::"transitive"::: )  )) "holds"  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set   ($#k9_relat_1 :::"neighbourhood"::: )   "("  ","  ")" ) "is"   ($#m1_toler_1 :::"TolClass":::) "of" (Set (Var "T")))))) ; 
 
theorem :: TOLER_1:36 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"Tolerance":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Y")) "being"   ($#m1_toler_1 :::"TolClass":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y")))) "holds"  (Bool (Set (Var "Y"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_relat_1 :::"neighbourhood"::: )   "("  ","  ")" )))))) ; 
 
theorem :: TOLER_1:37 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "R")) "," (Set (Var "T")) "being"   ($#m1_subset_1 :::"Tolerance":::) "of" (Set (Var "X")) "holds"   (Bool  "("  (Bool (Set   ($#k3_toler_1 :::"TolSets"::: )  (Set (Var "R")))  ($#r1_tarski :::"c="::: )  (Set   ($#k3_toler_1 :::"TolSets"::: )  (Set (Var "T")))) "iff" (Bool (Set (Var "R"))  ($#r1_relset_1 :::"c="::: )  (Set (Var "T")))  ")" ))) ; 
 
theorem :: TOLER_1:38 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"Tolerance":::) "of" (Set (Var "X")) "holds"  (Bool (Set   ($#k4_toler_1 :::"TolClasses"::: )  (Set (Var "T")))  ($#r1_tarski :::"c="::: )  (Set   ($#k3_toler_1 :::"TolSets"::: )  (Set (Var "T")))))) ; 
 
theorem :: TOLER_1:39 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "R")) "," (Set (Var "T")) "being"   ($#m1_subset_1 :::"Tolerance":::) "of" (Set (Var "X"))  "st" (Bool (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set   ($#k9_relat_1 :::"neighbourhood"::: )   "("  ","  ")" )  ($#r1_tarski :::"c="::: )  (Set   ($#k9_relat_1 :::"neighbourhood"::: )   "("  ","  ")" ))  ")" )) "holds"  (Bool (Set (Var "R"))  ($#r1_relset_1 :::"c="::: )  (Set (Var "T"))))) ; 
 
theorem :: TOLER_1:40 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"Tolerance":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Var "T"))  ($#r1_relset_1 :::"c="::: )  (Set (Set (Var "T"))  ($#k4_relset_1 :::"*"::: )  (Set (Var "T")))))) ;