:: ROUGHS_1  semantic presentation begin  registrationlet "A" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#g1_orders_2 :::"RelStr"::: )  "(#"  "A" "," (Set  "("  ($#k6_partfun1 :::"id"::: )  "A" ")" ) "#)" ) ->   ($#v1_orders_3 :::"discrete"::: )   ; 
end; 
theorem :: ROUGHS_1:1 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set   ($#k1_eqrel_1 :::"Total"::: )  (Set (Var "X")))  ($#r1_relset_1 :::"c="::: )  (Set   ($#k6_partfun1 :::"id"::: )  (Set (Var "X"))))) "holds"  (Bool (Set (Var "X")) "is"   ($#v1_zfmisc_1 :::"trivial"::: )  )) ; 
 definitionlet "A" be    ($#l1_orders_2 :::"RelStr"::: )  ; attr "A" is  :::"diagonal":::  means :: ROUGHS_1:def 1 (Bool (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" "A")  ($#r1_relset_1 :::"c="::: )  (Set   ($#k6_partfun1 :::"id"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "A"))); end; 




:: deftheorem    defines :::"diagonal"::: ROUGHS_1:def 1 :  (Bool  "for" (Set (Var "A")) "being"    ($#l1_orders_2 :::"RelStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "A")) "is"   ($#v1_roughs_1 :::"diagonal"::: )  ) "iff" (Bool (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "A")))  ($#r1_relset_1 :::"c="::: )  (Set   ($#k6_partfun1 :::"id"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "A")))))  ")" )); 
 registrationlet "A" be  ($#~v1_zfmisc_1  "non"   ($#v1_zfmisc_1 :::"trivial"::: )   )    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#g1_orders_2 :::"RelStr"::: )  "(#"  "A" "," (Set  "("  ($#k1_eqrel_1 :::"Total"::: )  "A" ")" ) "#)" ) ->  ($#~v1_roughs_1  "non"   ($#v1_roughs_1 :::"diagonal"::: )   )  ; 
end; 
theorem :: ROUGHS_1:2 (Bool  "for" (Set (Var "L")) "being"   ($#v3_orders_2 :::"reflexive"::: )     ($#l1_orders_2 :::"RelStr"::: )   "holds"  (Bool (Set   ($#k6_partfun1 :::"id"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L"))))  ($#r1_relset_1 :::"c="::: )  (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "L"))))) ; 
 registration
cluster   ($#v3_orders_2 :::"reflexive"::: )    ($#~v1_orders_3  "non"   ($#v1_orders_3 :::"discrete"::: )   )   ->  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )    ($#v3_orders_2 :::"reflexive"::: )    for    ($#l1_orders_2 :::"RelStr"::: )  ; 

cluster   ($#v7_struct_0 :::"trivial"::: )     ($#v3_orders_2 :::"reflexive"::: )    ->   ($#v1_orders_3 :::"discrete"::: )    for    ($#l1_orders_2 :::"RelStr"::: )  ; 
end; 
theorem :: ROUGHS_1:3 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "R")) "being"   ($#v1_relat_2 :::"reflexive"::: )     ($#v1_partfun1 :::"total"::: )    ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X")) "holds"  (Bool (Set   ($#k6_partfun1 :::"id"::: )  (Set (Var "X")))  ($#r1_relset_1 :::"c="::: )  (Set (Var "R"))))) ; 
 registration
cluster   ($#v1_orders_3 :::"discrete"::: )    ->   ($#v1_roughs_1 :::"diagonal"::: )    for    ($#l1_orders_2 :::"RelStr"::: )  ; 

cluster  ($#~v1_roughs_1  "non"   ($#v1_roughs_1 :::"diagonal"::: )   )   ->  ($#~v1_orders_3  "non"   ($#v1_orders_3 :::"discrete"::: )   )   for    ($#l1_orders_2 :::"RelStr"::: )  ; 
end; registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v1_roughs_1  "non"   ($#v1_roughs_1 :::"diagonal"::: )   )   for    ($#l1_orders_2 :::"RelStr"::: )  ; 
end; 
theorem :: ROUGHS_1:4 (Bool  "for" (Set (Var "A")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v1_roughs_1  "non"   ($#v1_roughs_1 :::"diagonal"::: )   )    ($#l1_orders_2 :::"RelStr"::: )   (Bool  "ex" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set (Var "y"))) & (Bool (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "A"))))  ")" ))) ; 
 
theorem :: ROUGHS_1:5 (Bool  "for" (Set (Var "D")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set (Var "D")) "holds"  (Bool (Set   ($#k3_card_3 :::"Union"::: )  (Set  "(" (Set (Var "p"))  ($#k8_finseq_1 :::"^"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_card_3 :::"Union"::: )  (Set (Var "p")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  "("  ($#k3_card_3 :::"Union"::: )  (Set (Var "q")) ")" ))))) ; 
 
theorem :: ROUGHS_1:6 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "q")) "is"   ($#v1_prob_2 :::"disjoint_valued"::: )  ) & (Bool (Set (Var "p"))  ($#r1_tarski :::"c="::: )  (Set (Var "q")))) "holds"  (Bool (Set (Var "p")) "is"   ($#v1_prob_2 :::"disjoint_valued"::: )  )) ; 
 registration
cluster   ($#v1_xboole_0 :::"empty"::: )     ($#v1_relat_1 :::"Relation-like"::: )     ($#v1_funct_1 :::"Function-like"::: )    ->   ($#v1_prob_2 :::"disjoint_valued"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; registrationlet "A" be    ($#m1_hidden :::"set"::: )  ; 
cluster   ($#v1_relat_1 :::"Relation-like"::: )   (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v4_relat_1 :::"-defined"::: )   "A"  ($#v5_relat_1 :::"-valued"::: )     ($#v1_funct_1 :::"Function-like"::: )     ($#v1_finset_1 :::"finite"::: )     ($#v1_prob_2 :::"disjoint_valued"::: )     ($#v1_finseq_1 :::"FinSequence-like"::: )     ($#v2_finseq_1 :::"FinSubsequence-like"::: )    for    ($#m1_finseq_1 :::"FinSequence"::: )   "of" "A"; 
end; registrationlet "A" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; 
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_relat_1 :::"Relation-like"::: )   (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v4_relat_1 :::"-defined"::: )   "A"  ($#v5_relat_1 :::"-valued"::: )     ($#v1_funct_1 :::"Function-like"::: )     ($#v1_finset_1 :::"finite"::: )     ($#v1_prob_2 :::"disjoint_valued"::: )     ($#v1_finseq_1 :::"FinSequence-like"::: )     ($#v2_finseq_1 :::"FinSubsequence-like"::: )    for    ($#m1_finseq_1 :::"FinSequence"::: )   "of" "A"; 
end; definitionlet "A" be    ($#m1_hidden :::"set"::: )  ; let "X" be    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set (Const "A"))); let "n" be   ($#m1_hidden :::"Nat":::); :: original: :::"."::: redefine func "X" :::"."::: "n" ->   ($#m1_subset_1 :::"Subset":::) "of" "A"; end; definitionlet "A" be    ($#m1_hidden :::"set"::: )  ; let "X" be    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set (Const "A"))); :: original: :::"Union"::: redefine func  :::"Union"::: "X" ->   ($#m1_subset_1 :::"Subset":::) "of" "A"; end; registrationlet "A" be   ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )  ; let "R" be   ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "A")); 
cluster (Set   ($#g1_orders_2 :::"RelStr"::: )  "(#"  "A" "," "R" "#)" ) ->   ($#v8_struct_0 :::"finite"::: )   ; 
end; 
theorem :: ROUGHS_1:7 (Bool  "for" (Set (Var "X")) "," (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"Tolerance":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k6_eqrel_1 :::"Class"::: )   "(" (Set (Var "T")) "," (Set (Var "y")) ")" ))) "holds"  (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k6_eqrel_1 :::"Class"::: )   "(" (Set (Var "T")) "," (Set (Var "x")) ")" )))) ; 
 begin  definitionlet "P" be    ($#l1_orders_2 :::"RelStr"::: )  ; attr "P" is  :::"with_equivalence":::  means :: ROUGHS_1:def 2 (Bool (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" "P") "is"   ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "P")); attr "P" is  :::"with_tolerance":::  means :: ROUGHS_1:def 3 (Bool (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" "P") "is"   ($#m1_subset_1 :::"Tolerance":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "P")); end; 








:: deftheorem    defines :::"with_equivalence"::: ROUGHS_1:def 2 :  (Bool  "for" (Set (Var "P")) "being"    ($#l1_orders_2 :::"RelStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "P")) "is"   ($#v2_roughs_1 :::"with_equivalence"::: )  ) "iff" (Bool (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "P"))) "is"   ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "P"))))  ")" )); 
 
:: deftheorem    defines :::"with_tolerance"::: ROUGHS_1:def 3 :  (Bool  "for" (Set (Var "P")) "being"    ($#l1_orders_2 :::"RelStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "P")) "is"   ($#v3_roughs_1 :::"with_tolerance"::: )  ) "iff" (Bool (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "P"))) "is"   ($#m1_subset_1 :::"Tolerance":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "P"))))  ")" )); 
 registration
cluster   ($#v2_roughs_1 :::"with_equivalence"::: )    ->   ($#v3_roughs_1 :::"with_tolerance"::: )    for    ($#l1_orders_2 :::"RelStr"::: )  ; 
end; registrationlet "A" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#g1_orders_2 :::"RelStr"::: )  "(#"  "A" "," (Set  "("  ($#k6_partfun1 :::"id"::: )  "A" ")" ) "#)" ) ->   ($#v2_roughs_1 :::"with_equivalence"::: )   ; 
end; registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v8_struct_0 :::"finite"::: )     ($#v1_orders_3 :::"discrete"::: )     ($#v2_roughs_1 :::"with_equivalence"::: )    for    ($#l1_orders_2 :::"RelStr"::: )  ; 

cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v8_struct_0 :::"finite"::: )    ($#~v1_roughs_1  "non"   ($#v1_roughs_1 :::"diagonal"::: )   )    ($#v2_roughs_1 :::"with_equivalence"::: )    for    ($#l1_orders_2 :::"RelStr"::: )  ; 
end; definitionmode Approximation_Space is  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_roughs_1 :::"with_equivalence"::: )     ($#l1_orders_2 :::"RelStr"::: )  ; mode Tolerance_Space is  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_roughs_1 :::"with_tolerance"::: )     ($#l1_orders_2 :::"RelStr"::: )  ; end; registrationlet "A" be   ($#l1_orders_2 :::"Tolerance_Space":::); 
cluster (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" "A") ->   ($#v1_relat_2 :::"reflexive"::: )     ($#v3_relat_2 :::"symmetric"::: )     ($#v1_partfun1 :::"total"::: )   ; 
end; registrationlet "A" be   ($#l1_orders_2 :::"Approximation_Space":::); 
cluster (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" "A") ->   ($#v8_relat_2 :::"transitive"::: )   ; 
end; definitionlet "A" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )  ; let "X" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "A")); func  :::"LAp"::: "X" ->   ($#m1_subset_1 :::"Subset":::) "of" "A" equals :: ROUGHS_1:def 4  "{"  (Set (Var "x")) where x "is"   ($#m1_subset_1 :::"Element":::) "of" "A" : (Bool (Set   ($#k6_eqrel_1 :::"Class"::: )   "(" (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" "A") "," (Set (Var "x")) ")" )  ($#r1_tarski :::"c="::: )  "X")  "}"  ; func  :::"UAp"::: "X" ->   ($#m1_subset_1 :::"Subset":::) "of" "A" equals :: ROUGHS_1:def 5  "{"  (Set (Var "x")) where x "is"   ($#m1_subset_1 :::"Element":::) "of" "A" : (Bool (Set   ($#k6_eqrel_1 :::"Class"::: )   "(" (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" "A") "," (Set (Var "x")) ")" )  ($#r1_xboole_0 :::"meets"::: )  "X")  "}"  ; end; 












:: deftheorem    defines :::"LAp"::: ROUGHS_1:def 4 :  (Bool  "for" (Set (Var "A")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "holds"  (Bool (Set   ($#k3_roughs_1 :::"LAp"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "x")) where x "is"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) : (Bool (Set   ($#k6_eqrel_1 :::"Class"::: )   "(" (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "A"))) "," (Set (Var "x")) ")" )  ($#r1_tarski :::"c="::: )  (Set (Var "X")))  "}"  ))); 
 
:: deftheorem    defines :::"UAp"::: ROUGHS_1:def 5 :  (Bool  "for" (Set (Var "A")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "holds"  (Bool (Set   ($#k4_roughs_1 :::"UAp"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "x")) where x "is"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) : (Bool (Set   ($#k6_eqrel_1 :::"Class"::: )   "(" (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "A"))) "," (Set (Var "x")) ")" )  ($#r1_xboole_0 :::"meets"::: )  (Set (Var "X")))  "}"  ))); 
 definitionlet "A" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )  ; let "X" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "A")); func  :::"BndAp"::: "X" ->   ($#m1_subset_1 :::"Subset":::) "of" "A" equals :: ROUGHS_1:def 6 (Set (Set  "("  ($#k4_roughs_1 :::"UAp"::: )  "X" ")" )  ($#k7_subset_1 :::"\"::: )  (Set  "("  ($#k3_roughs_1 :::"LAp"::: )  "X" ")" )); end; 






:: deftheorem    defines :::"BndAp"::: ROUGHS_1:def 6 :  (Bool  "for" (Set (Var "A")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "holds"  (Bool (Set   ($#k5_roughs_1 :::"BndAp"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_roughs_1 :::"UAp"::: )  (Set (Var "X")) ")" )  ($#k7_subset_1 :::"\"::: )  (Set  "("  ($#k3_roughs_1 :::"LAp"::: )  (Set (Var "X")) ")" ))))); 
 definitionlet "A" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )  ; let "X" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "A")); attr "X" is  :::"rough":::  means :: ROUGHS_1:def 7 (Bool (Set   ($#k5_roughs_1 :::"BndAp"::: )  "X")  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )); end; 





:: deftheorem    defines :::"rough"::: ROUGHS_1:def 7 :  (Bool  "for" (Set (Var "A")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "holds"   (Bool  "("  (Bool (Set (Var "X")) "is"   ($#v4_roughs_1 :::"rough"::: )  ) "iff" (Bool (Set   ($#k5_roughs_1 :::"BndAp"::: )  (Set (Var "X")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))  ")" ))); 
 notationlet "A" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )  ; let "X" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "A")); antonym  :::"exact"::: "X" for  :::"rough"::: ; end; 







theorem :: ROUGHS_1:8 (Bool  "for" (Set (Var "A")) "being"   ($#l1_orders_2 :::"Tolerance_Space":::)  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A"))  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_roughs_1 :::"LAp"::: )  (Set (Var "X"))))) "holds"  (Bool (Set   ($#k6_eqrel_1 :::"Class"::: )   "(" (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "A"))) "," (Set (Var "x")) ")" )  ($#r1_tarski :::"c="::: )  (Set (Var "X")))))) ; 
 
theorem :: ROUGHS_1:9 (Bool  "for" (Set (Var "A")) "being"   ($#l1_orders_2 :::"Tolerance_Space":::)  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A"))  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A"))  "st" (Bool (Bool (Set   ($#k6_eqrel_1 :::"Class"::: )   "(" (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "A"))) "," (Set (Var "x")) ")" )  ($#r1_tarski :::"c="::: )  (Set (Var "X")))) "holds"  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_roughs_1 :::"LAp"::: )  (Set (Var "X"))))))) ; 
 
theorem :: ROUGHS_1:10 (Bool  "for" (Set (Var "A")) "being"   ($#l1_orders_2 :::"Tolerance_Space":::)  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A"))  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_roughs_1 :::"UAp"::: )  (Set (Var "X"))))) "holds"  (Bool (Set   ($#k6_eqrel_1 :::"Class"::: )   "(" (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "A"))) "," (Set (Var "x")) ")" )  ($#r1_xboole_0 :::"meets"::: )  (Set (Var "X")))))) ; 
 
theorem :: ROUGHS_1:11 (Bool  "for" (Set (Var "A")) "being"   ($#l1_orders_2 :::"Tolerance_Space":::)  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A"))  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A"))  "st" (Bool (Bool (Set   ($#k6_eqrel_1 :::"Class"::: )   "(" (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "A"))) "," (Set (Var "x")) ")" )  ($#r1_xboole_0 :::"meets"::: )  (Set (Var "X")))) "holds"  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_roughs_1 :::"UAp"::: )  (Set (Var "X"))))))) ; 
 
theorem :: ROUGHS_1:12 (Bool  "for" (Set (Var "A")) "being"   ($#l1_orders_2 :::"Tolerance_Space":::)  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "holds"  (Bool (Set   ($#k3_roughs_1 :::"LAp"::: )  (Set (Var "X")))  ($#r1_tarski :::"c="::: )  (Set (Var "X"))))) ; 
 
theorem :: ROUGHS_1:13 (Bool  "for" (Set (Var "A")) "being"   ($#l1_orders_2 :::"Tolerance_Space":::)  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "holds"  (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set   ($#k4_roughs_1 :::"UAp"::: )  (Set (Var "X")))))) ; 
 
theorem :: ROUGHS_1:14 (Bool  "for" (Set (Var "A")) "being"   ($#l1_orders_2 :::"Tolerance_Space":::)  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "holds"  (Bool (Set   ($#k3_roughs_1 :::"LAp"::: )  (Set (Var "X")))  ($#r1_tarski :::"c="::: )  (Set   ($#k4_roughs_1 :::"UAp"::: )  (Set (Var "X")))))) ; 
 
theorem :: ROUGHS_1:15 (Bool  "for" (Set (Var "A")) "being"   ($#l1_orders_2 :::"Tolerance_Space":::)  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "holds"   (Bool  "("  (Bool (Set (Var "X")) "is"   ($#v4_roughs_1 :::"exact"::: )  ) "iff" (Bool (Set   ($#k3_roughs_1 :::"LAp"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set (Var "X")))  ")" ))) ; 
 
theorem :: ROUGHS_1:16 (Bool  "for" (Set (Var "A")) "being"   ($#l1_orders_2 :::"Tolerance_Space":::)  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "holds"   (Bool  "("  (Bool (Set (Var "X")) "is"   ($#v4_roughs_1 :::"exact"::: )  ) "iff" (Bool (Set   ($#k4_roughs_1 :::"UAp"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set (Var "X")))  ")" ))) ; 
 
theorem :: ROUGHS_1:17 (Bool  "for" (Set (Var "A")) "being"   ($#l1_orders_2 :::"Tolerance_Space":::)  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "holds"   (Bool  "("  (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_roughs_1 :::"LAp"::: )  (Set (Var "X")))) "iff" (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_roughs_1 :::"UAp"::: )  (Set (Var "X"))))  ")" ))) ; 
 
theorem :: ROUGHS_1:18 (Bool  "for" (Set (Var "A")) "being"   ($#l1_orders_2 :::"Tolerance_Space":::) "holds"  (Bool (Set   ($#k3_roughs_1 :::"LAp"::: )  (Set  "("  ($#k1_struct_0 :::"{}"::: )  (Set (Var "A")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) ; 
 
theorem :: ROUGHS_1:19 (Bool  "for" (Set (Var "A")) "being"   ($#l1_orders_2 :::"Tolerance_Space":::) "holds"  (Bool (Set   ($#k4_roughs_1 :::"UAp"::: )  (Set  "("  ($#k1_struct_0 :::"{}"::: )  (Set (Var "A")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) ; 
 
theorem :: ROUGHS_1:20 (Bool  "for" (Set (Var "A")) "being"   ($#l1_orders_2 :::"Tolerance_Space":::) "holds"  (Bool (Set   ($#k3_roughs_1 :::"LAp"::: )  (Set  "("  ($#k2_struct_0 :::"[#]"::: )  (Set (Var "A")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_struct_0 :::"[#]"::: )  (Set (Var "A"))))) ; 
 
theorem :: ROUGHS_1:21 (Bool  "for" (Set (Var "A")) "being"   ($#l1_orders_2 :::"Tolerance_Space":::) "holds"  (Bool (Set   ($#k4_roughs_1 :::"UAp"::: )  (Set  "("  ($#k2_struct_0 :::"[#]"::: )  (Set (Var "A")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_struct_0 :::"[#]"::: )  (Set (Var "A"))))) ; 
 
theorem :: ROUGHS_1:22 (Bool  "for" (Set (Var "A")) "being"   ($#l1_orders_2 :::"Tolerance_Space":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "holds"  (Bool (Set   ($#k3_roughs_1 :::"LAp"::: )  (Set  "(" (Set (Var "X"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "Y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_roughs_1 :::"LAp"::: )  (Set (Var "X")) ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k3_roughs_1 :::"LAp"::: )  (Set (Var "Y")) ")" ))))) ; 
 
theorem :: ROUGHS_1:23 (Bool  "for" (Set (Var "A")) "being"   ($#l1_orders_2 :::"Tolerance_Space":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "holds"  (Bool (Set   ($#k4_roughs_1 :::"UAp"::: )  (Set  "(" (Set (Var "X"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "Y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_roughs_1 :::"UAp"::: )  (Set (Var "X")) ")" )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k4_roughs_1 :::"UAp"::: )  (Set (Var "Y")) ")" ))))) ; 
 
theorem :: ROUGHS_1:24 (Bool  "for" (Set (Var "A")) "being"   ($#l1_orders_2 :::"Tolerance_Space":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A"))  "st" (Bool (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y")))) "holds"  (Bool (Set   ($#k3_roughs_1 :::"LAp"::: )  (Set (Var "X")))  ($#r1_tarski :::"c="::: )  (Set   ($#k3_roughs_1 :::"LAp"::: )  (Set (Var "Y")))))) ; 
 
theorem :: ROUGHS_1:25 (Bool  "for" (Set (Var "A")) "being"   ($#l1_orders_2 :::"Tolerance_Space":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A"))  "st" (Bool (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y")))) "holds"  (Bool (Set   ($#k4_roughs_1 :::"UAp"::: )  (Set (Var "X")))  ($#r1_tarski :::"c="::: )  (Set   ($#k4_roughs_1 :::"UAp"::: )  (Set (Var "Y")))))) ; 
 
theorem :: ROUGHS_1:26 (Bool  "for" (Set (Var "A")) "being"   ($#l1_orders_2 :::"Tolerance_Space":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "holds"  (Bool (Set (Set  "("  ($#k3_roughs_1 :::"LAp"::: )  (Set (Var "X")) ")" )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k3_roughs_1 :::"LAp"::: )  (Set (Var "Y")) ")" ))  ($#r1_tarski :::"c="::: )  (Set   ($#k3_roughs_1 :::"LAp"::: )  (Set  "(" (Set (Var "X"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "Y")) ")" ))))) ; 
 
theorem :: ROUGHS_1:27 (Bool  "for" (Set (Var "A")) "being"   ($#l1_orders_2 :::"Tolerance_Space":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "holds"  (Bool (Set   ($#k4_roughs_1 :::"UAp"::: )  (Set  "(" (Set (Var "X"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "Y")) ")" ))  ($#r1_tarski :::"c="::: )  (Set (Set  "("  ($#k4_roughs_1 :::"UAp"::: )  (Set (Var "X")) ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k4_roughs_1 :::"UAp"::: )  (Set (Var "Y")) ")" ))))) ; 
 
theorem :: ROUGHS_1:28 (Bool  "for" (Set (Var "A")) "being"   ($#l1_orders_2 :::"Tolerance_Space":::)  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "holds"  (Bool (Set   ($#k3_roughs_1 :::"LAp"::: )  (Set  "(" (Set (Var "X"))  ($#k3_subset_1 :::"`"::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_roughs_1 :::"UAp"::: )  (Set (Var "X")) ")" )  ($#k3_subset_1 :::"`"::: )  )))) ; 
 
theorem :: ROUGHS_1:29 (Bool  "for" (Set (Var "A")) "being"   ($#l1_orders_2 :::"Tolerance_Space":::)  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "holds"  (Bool (Set   ($#k4_roughs_1 :::"UAp"::: )  (Set  "(" (Set (Var "X"))  ($#k3_subset_1 :::"`"::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_roughs_1 :::"LAp"::: )  (Set (Var "X")) ")" )  ($#k3_subset_1 :::"`"::: )  )))) ; 
 
theorem :: ROUGHS_1:30 (Bool  "for" (Set (Var "A")) "being"   ($#l1_orders_2 :::"Tolerance_Space":::)  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "holds"  (Bool (Set   ($#k4_roughs_1 :::"UAp"::: )  (Set  "("  ($#k3_roughs_1 :::"LAp"::: )  (Set  "("  ($#k4_roughs_1 :::"UAp"::: )  (Set (Var "X")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_roughs_1 :::"UAp"::: )  (Set (Var "X")))))) ; 
 
theorem :: ROUGHS_1:31 (Bool  "for" (Set (Var "A")) "being"   ($#l1_orders_2 :::"Tolerance_Space":::)  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "holds"  (Bool (Set   ($#k3_roughs_1 :::"LAp"::: )  (Set  "("  ($#k4_roughs_1 :::"UAp"::: )  (Set  "("  ($#k3_roughs_1 :::"LAp"::: )  (Set (Var "X")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k3_roughs_1 :::"LAp"::: )  (Set (Var "X")))))) ; 
 
theorem :: ROUGHS_1:32 (Bool  "for" (Set (Var "A")) "being"   ($#l1_orders_2 :::"Tolerance_Space":::)  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "holds"  (Bool (Set   ($#k5_roughs_1 :::"BndAp"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_roughs_1 :::"BndAp"::: )  (Set  "(" (Set (Var "X"))  ($#k3_subset_1 :::"`"::: )  ")" ))))) ; 
 






theorem :: ROUGHS_1:33 (Bool  "for" (Set (Var "A")) "being"   ($#l1_orders_2 :::"Approximation_Space":::)  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "holds"  (Bool (Set   ($#k3_roughs_1 :::"LAp"::: )  (Set  "("  ($#k3_roughs_1 :::"LAp"::: )  (Set (Var "X")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k3_roughs_1 :::"LAp"::: )  (Set (Var "X")))))) ; 
 
theorem :: ROUGHS_1:34 (Bool  "for" (Set (Var "A")) "being"   ($#l1_orders_2 :::"Approximation_Space":::)  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "holds"  (Bool (Set   ($#k3_roughs_1 :::"LAp"::: )  (Set  "("  ($#k3_roughs_1 :::"LAp"::: )  (Set (Var "X")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_roughs_1 :::"UAp"::: )  (Set  "("  ($#k3_roughs_1 :::"LAp"::: )  (Set (Var "X")) ")" ))))) ; 
 
theorem :: ROUGHS_1:35 (Bool  "for" (Set (Var "A")) "being"   ($#l1_orders_2 :::"Approximation_Space":::)  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "holds"  (Bool (Set   ($#k4_roughs_1 :::"UAp"::: )  (Set  "("  ($#k4_roughs_1 :::"UAp"::: )  (Set (Var "X")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_roughs_1 :::"UAp"::: )  (Set (Var "X")))))) ; 
 
theorem :: ROUGHS_1:36 (Bool  "for" (Set (Var "A")) "being"   ($#l1_orders_2 :::"Approximation_Space":::)  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "holds"  (Bool (Set   ($#k4_roughs_1 :::"UAp"::: )  (Set  "("  ($#k4_roughs_1 :::"UAp"::: )  (Set (Var "X")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k3_roughs_1 :::"LAp"::: )  (Set  "("  ($#k4_roughs_1 :::"UAp"::: )  (Set (Var "X")) ")" ))))) ; 
 registrationlet "A" be   ($#l1_orders_2 :::"Tolerance_Space":::); 
cluster   ($#v4_roughs_1 :::"exact"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "A")); 
end; registrationlet "A" be   ($#l1_orders_2 :::"Approximation_Space":::); let "X" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "A")); 
cluster (Set   ($#k3_roughs_1 :::"LAp"::: )  "X") ->   ($#v4_roughs_1 :::"exact"::: )   ; 

cluster (Set   ($#k4_roughs_1 :::"UAp"::: )  "X") ->   ($#v4_roughs_1 :::"exact"::: )   ; 
end; 
theorem :: ROUGHS_1:37 (Bool  "for" (Set (Var "A")) "being"   ($#l1_orders_2 :::"Approximation_Space":::)  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A"))  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_roughs_1 :::"UAp"::: )  (Set (Var "X")))) & (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "A"))))) "holds"  (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_roughs_1 :::"UAp"::: )  (Set (Var "X"))))))) ; 
 registrationlet "A" be  ($#~v1_roughs_1  "non"   ($#v1_roughs_1 :::"diagonal"::: )   )   ($#l1_orders_2 :::"Approximation_Space":::); 
cluster   ($#v4_roughs_1 :::"rough"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "A")); 
end; definitionlet "A" be   ($#l1_orders_2 :::"Approximation_Space":::); let "X" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "A")); mode  :::"RoughSet":::  "of" "X" ->    ($#m1_hidden :::"set"::: )   means :: ROUGHS_1:def 8 (Bool it  ($#r1_hidden :::"="::: )  (Set  ($#k1_domain_1 :::"["::: ) (Set  "("  ($#k3_roughs_1 :::"LAp"::: )  "X" ")" ) "," (Set  "("  ($#k4_roughs_1 :::"UAp"::: )  "X" ")" ) ($#k1_domain_1 :::"]"::: ) )); end; 






:: deftheorem    defines :::"RoughSet"::: ROUGHS_1:def 8 :  (Bool  "for" (Set (Var "A")) "being"   ($#l1_orders_2 :::"Approximation_Space":::)  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A"))  (Bool  "for" (Set (Var "b3")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b3")) "is"    ($#m1_roughs_1 :::"RoughSet"::: )   "of" (Set (Var "X"))) "iff" (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_domain_1 :::"["::: ) (Set  "("  ($#k3_roughs_1 :::"LAp"::: )  (Set (Var "X")) ")" ) "," (Set  "("  ($#k4_roughs_1 :::"UAp"::: )  (Set (Var "X")) ")" ) ($#k1_domain_1 :::"]"::: ) ))  ")" )))); 
 begin  registrationlet "A" be   ($#v8_struct_0 :::"finite"::: )    ($#l1_orders_2 :::"Tolerance_Space":::); let "x" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "A")); 
cluster (Set   ($#k1_card_1 :::"card"::: )  (Set  "("  ($#k6_eqrel_1 :::"Class"::: )   "(" (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" "A") "," "x" ")"  ")" )) ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; definitionlet "A" be   ($#v8_struct_0 :::"finite"::: )    ($#l1_orders_2 :::"Tolerance_Space":::); let "X" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "A")); func  :::"MemberFunc":::  "(" "X" "," "A" ")"  ->   ($#m1_subset_1 :::"Function":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "A") "," (Set  ($#k1_numbers :::"REAL"::: ) ) means :: ROUGHS_1:def 9 (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" "A" "holds"  (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_card_1 :::"card"::: )  (Set  "(" "X"  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k6_eqrel_1 :::"Class"::: )   "(" (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" "A") "," (Set (Var "x")) ")"  ")" ) ")" ) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set  "("  ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k6_eqrel_1 :::"Class"::: )   "(" (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" "A") "," (Set (Var "x")) ")"  ")" ) ")" )))); end; 






:: deftheorem    defines :::"MemberFunc"::: ROUGHS_1:def 9 :  (Bool  "for" (Set (Var "A")) "being"   ($#v8_struct_0 :::"finite"::: )    ($#l1_orders_2 :::"Tolerance_Space":::)  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A"))  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "A"))) "," (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_roughs_1 :::"MemberFunc"::: )   "(" (Set (Var "X")) "," (Set (Var "A")) ")" )) "iff" (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "holds"  (Bool (Set (Set (Var "b3"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_card_1 :::"card"::: )  (Set  "(" (Set (Var "X"))  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k6_eqrel_1 :::"Class"::: )   "(" (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "A"))) "," (Set (Var "x")) ")"  ")" ) ")" ) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set  "("  ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k6_eqrel_1 :::"Class"::: )   "(" (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "A"))) "," (Set (Var "x")) ")"  ")" ) ")" ))))  ")" )))); 
 









theorem :: ROUGHS_1:38 (Bool  "for" (Set (Var "A")) "being"   ($#v8_struct_0 :::"finite"::: )    ($#l1_orders_2 :::"Tolerance_Space":::)  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A"))  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "holds"   (Bool  "("  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "("  ($#k6_roughs_1 :::"MemberFunc"::: )   "(" (Set (Var "X")) "," (Set (Var "A")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))) & (Bool (Set (Set  "("  ($#k6_roughs_1 :::"MemberFunc"::: )   "(" (Set (Var "X")) "," (Set (Var "A")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::"<="::: )  (Num 1))  ")" )))) ; 
 
theorem :: ROUGHS_1:39 (Bool  "for" (Set (Var "A")) "being"   ($#v8_struct_0 :::"finite"::: )    ($#l1_orders_2 :::"Tolerance_Space":::)  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A"))  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "holds"  (Bool (Set (Set  "("  ($#k6_roughs_1 :::"MemberFunc"::: )   "(" (Set (Var "X")) "," (Set (Var "A")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r2_hidden :::"in"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) ))))) ; 
 










theorem :: ROUGHS_1:40 (Bool  "for" (Set (Var "A")) "being"   ($#v8_struct_0 :::"finite"::: )    ($#l1_orders_2 :::"Approximation_Space":::)  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A"))  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "holds"   (Bool  "("  (Bool (Set (Set  "("  ($#k6_roughs_1 :::"MemberFunc"::: )   "(" (Set (Var "X")) "," (Set (Var "A")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Num 1)) "iff" (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_roughs_1 :::"LAp"::: )  (Set (Var "X"))))  ")" )))) ; 
 
theorem :: ROUGHS_1:41 (Bool  "for" (Set (Var "A")) "being"   ($#v8_struct_0 :::"finite"::: )    ($#l1_orders_2 :::"Approximation_Space":::)  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A"))  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "holds"   (Bool  "("  (Bool (Set (Set  "("  ($#k6_roughs_1 :::"MemberFunc"::: )   "(" (Set (Var "X")) "," (Set (Var "A")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "iff" (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Set  "("  ($#k4_roughs_1 :::"UAp"::: )  (Set (Var "X")) ")" )  ($#k3_subset_1 :::"`"::: )  ))  ")" )))) ; 
 
theorem :: ROUGHS_1:42 (Bool  "for" (Set (Var "A")) "being"   ($#v8_struct_0 :::"finite"::: )    ($#l1_orders_2 :::"Approximation_Space":::)  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A"))  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "holds"   (Bool  "("  (Bool  "("  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Set  "("  ($#k6_roughs_1 :::"MemberFunc"::: )   "(" (Set (Var "X")) "," (Set (Var "A")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))) & (Bool (Set (Set  "("  ($#k6_roughs_1 :::"MemberFunc"::: )   "(" (Set (Var "X")) "," (Set (Var "A")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::"<"::: )  (Num 1))  ")" ) "iff" (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k5_roughs_1 :::"BndAp"::: )  (Set (Var "X"))))  ")" )))) ; 
 
theorem :: ROUGHS_1:43 (Bool  "for" (Set (Var "A")) "being"   ($#v1_orders_3 :::"discrete"::: )    ($#l1_orders_2 :::"Approximation_Space":::)  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A"))  "holds" (Bool (Set (Var "X")) "is"   ($#v4_roughs_1 :::"exact"::: )  ))) ; 
 registrationlet "A" be   ($#v1_orders_3 :::"discrete"::: )    ($#l1_orders_2 :::"Approximation_Space":::); 
cluster   ->   ($#v4_roughs_1 :::"exact"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "A")); 
end; 
theorem :: ROUGHS_1:44 (Bool  "for" (Set (Var "A")) "being"   ($#v8_struct_0 :::"finite"::: )     ($#v1_orders_3 :::"discrete"::: )    ($#l1_orders_2 :::"Approximation_Space":::)  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "holds"  (Bool (Set   ($#k6_roughs_1 :::"MemberFunc"::: )   "(" (Set (Var "X")) "," (Set (Var "A")) ")" )  ($#r1_funct_2 :::"="::: )  (Set   ($#k5_funct_3 :::"chi"::: )   "(" (Set (Var "X")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "A"))) ")" )))) ; 
 
theorem :: ROUGHS_1:45 (Bool  "for" (Set (Var "A")) "being"   ($#v8_struct_0 :::"finite"::: )    ($#l1_orders_2 :::"Approximation_Space":::)  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A"))  (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  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "A"))))) "holds"  (Bool (Set (Set  "("  ($#k6_roughs_1 :::"MemberFunc"::: )   "(" (Set (Var "X")) "," (Set (Var "A")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k6_roughs_1 :::"MemberFunc"::: )   "(" (Set (Var "X")) "," (Set (Var "A")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "y"))))))) ; 
 
theorem :: ROUGHS_1:46 (Bool  "for" (Set (Var "A")) "being"   ($#v8_struct_0 :::"finite"::: )    ($#l1_orders_2 :::"Approximation_Space":::)  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A"))  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "holds"  (Bool (Set (Set  "("  ($#k6_roughs_1 :::"MemberFunc"::: )   "(" (Set  "(" (Set (Var "X"))  ($#k3_subset_1 :::"`"::: )  ")" ) "," (Set (Var "A")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "("  ($#k6_roughs_1 :::"MemberFunc"::: )   "(" (Set (Var "X")) "," (Set (Var "A")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "x")) ")" )))))) ; 
 
theorem :: ROUGHS_1:47 (Bool  "for" (Set (Var "A")) "being"   ($#v8_struct_0 :::"finite"::: )    ($#l1_orders_2 :::"Approximation_Space":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A"))  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A"))  "st" (Bool (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y")))) "holds"  (Bool (Set (Set  "("  ($#k6_roughs_1 :::"MemberFunc"::: )   "(" (Set (Var "X")) "," (Set (Var "A")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "("  ($#k6_roughs_1 :::"MemberFunc"::: )   "(" (Set (Var "Y")) "," (Set (Var "A")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "x"))))))) ; 
 
theorem :: ROUGHS_1:48 (Bool  "for" (Set (Var "A")) "being"   ($#v8_struct_0 :::"finite"::: )    ($#l1_orders_2 :::"Approximation_Space":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A"))  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "holds"  (Bool (Set (Set  "("  ($#k6_roughs_1 :::"MemberFunc"::: )   "(" (Set  "(" (Set (Var "X"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "Y")) ")" ) "," (Set (Var "A")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::">="::: )  (Set (Set  "("  ($#k6_roughs_1 :::"MemberFunc"::: )   "(" (Set (Var "X")) "," (Set (Var "A")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "x"))))))) ; 
 
theorem :: ROUGHS_1:49 (Bool  "for" (Set (Var "A")) "being"   ($#v8_struct_0 :::"finite"::: )    ($#l1_orders_2 :::"Approximation_Space":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A"))  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "holds"  (Bool (Set (Set  "("  ($#k6_roughs_1 :::"MemberFunc"::: )   "(" (Set  "(" (Set (Var "X"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "Y")) ")" ) "," (Set (Var "A")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "("  ($#k6_roughs_1 :::"MemberFunc"::: )   "(" (Set (Var "X")) "," (Set (Var "A")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "x"))))))) ; 
 
theorem :: ROUGHS_1:50 (Bool  "for" (Set (Var "A")) "being"   ($#v8_struct_0 :::"finite"::: )    ($#l1_orders_2 :::"Approximation_Space":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A"))  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "holds"  (Bool (Set (Set  "("  ($#k6_roughs_1 :::"MemberFunc"::: )   "(" (Set  "(" (Set (Var "X"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "Y")) ")" ) "," (Set (Var "A")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k4_xxreal_0 :::"max"::: )   "(" (Set  "(" (Set  "("  ($#k6_roughs_1 :::"MemberFunc"::: )   "(" (Set (Var "X")) "," (Set (Var "A")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "x")) ")" ) "," (Set  "(" (Set  "("  ($#k6_roughs_1 :::"MemberFunc"::: )   "(" (Set (Var "Y")) "," (Set (Var "A")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "x")) ")" ) ")" ))))) ; 
 
theorem :: ROUGHS_1:51 (Bool  "for" (Set (Var "A")) "being"   ($#v8_struct_0 :::"finite"::: )    ($#l1_orders_2 :::"Approximation_Space":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A"))  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A"))  "st" (Bool (Bool (Set (Var "X"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "Y")))) "holds"  (Bool (Set (Set  "("  ($#k6_roughs_1 :::"MemberFunc"::: )   "(" (Set  "(" (Set (Var "X"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "Y")) ")" ) "," (Set (Var "A")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k6_roughs_1 :::"MemberFunc"::: )   "(" (Set (Var "X")) "," (Set (Var "A")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "x")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "("  ($#k6_roughs_1 :::"MemberFunc"::: )   "(" (Set (Var "Y")) "," (Set (Var "A")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "x")) ")" )))))) ; 
 
theorem :: ROUGHS_1:52 (Bool  "for" (Set (Var "A")) "being"   ($#v8_struct_0 :::"finite"::: )    ($#l1_orders_2 :::"Approximation_Space":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A"))  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "holds"  (Bool (Set (Set  "("  ($#k6_roughs_1 :::"MemberFunc"::: )   "(" (Set  "(" (Set (Var "X"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "Y")) ")" ) "," (Set (Var "A")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_xxreal_0 :::"min"::: )   "(" (Set  "(" (Set  "("  ($#k6_roughs_1 :::"MemberFunc"::: )   "(" (Set (Var "X")) "," (Set (Var "A")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "x")) ")" ) "," (Set  "(" (Set  "("  ($#k6_roughs_1 :::"MemberFunc"::: )   "(" (Set (Var "Y")) "," (Set (Var "A")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "x")) ")" ) ")" ))))) ; 
 definitionlet "A" be   ($#v8_struct_0 :::"finite"::: )    ($#l1_orders_2 :::"Tolerance_Space":::); let "X" be    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Const "A")))); let "x" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "A")); func  :::"FinSeqM":::  "(" "x" "," "X" ")"  ->    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ) means :: ROUGHS_1:def 10 (Bool  "("  (Bool (Set   ($#k1_relset_1 :::"dom"::: )  it)  ($#r1_hidden :::"="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  "X")) & (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  "X"))) "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k6_roughs_1 :::"MemberFunc"::: )   "(" (Set  "(" "X"  ($#k1_roughs_1 :::"."::: )  (Set (Var "n")) ")" ) "," "A" ")"  ")" )  ($#k3_funct_2 :::"."::: )  "x"))  ")" )  ")" ); end; 







:: deftheorem    defines :::"FinSeqM"::: ROUGHS_1:def 10 :  (Bool  "for" (Set (Var "A")) "being"   ($#v8_struct_0 :::"finite"::: )    ($#l1_orders_2 :::"Tolerance_Space":::)  (Bool  "for" (Set (Var "X")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "A"))))  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A"))  (Bool  "for" (Set (Var "b4")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k7_roughs_1 :::"FinSeqM"::: )   "(" (Set (Var "x")) "," (Set (Var "X")) ")" )) "iff" (Bool  "("  (Bool (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "b4")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "X")))) & (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "X"))))) "holds"  (Bool (Set (Set (Var "b4"))  ($#k1_funct_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k6_roughs_1 :::"MemberFunc"::: )   "(" (Set  "(" (Set (Var "X"))  ($#k1_roughs_1 :::"."::: )  (Set (Var "n")) ")" ) "," (Set (Var "A")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "x"))))  ")" )  ")" )  ")" ))))); 
 
theorem :: ROUGHS_1:53 (Bool  "for" (Set (Var "A")) "being"   ($#v8_struct_0 :::"finite"::: )    ($#l1_orders_2 :::"Approximation_Space":::)  (Bool  "for" (Set (Var "X")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "A"))))  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A"))  (Bool  "for" (Set (Var "y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "holds"  (Bool (Set   ($#k7_roughs_1 :::"FinSeqM"::: )   "(" (Set (Var "x")) "," (Set  "(" (Set (Var "X"))  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "y")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ")" )  ($#r2_relset_1 :::"="::: )  (Set (Set  "("  ($#k7_roughs_1 :::"FinSeqM"::: )   "(" (Set (Var "x")) "," (Set (Var "X")) ")"  ")" )  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set  "(" (Set  "("  ($#k6_roughs_1 :::"MemberFunc"::: )   "(" (Set (Var "y")) "," (Set (Var "A")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "x")) ")" ) ($#k12_finseq_1 :::"*>"::: ) ))))))) ; 
 
theorem :: ROUGHS_1:54 (Bool  "for" (Set (Var "A")) "being"   ($#v8_struct_0 :::"finite"::: )    ($#l1_orders_2 :::"Approximation_Space":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "holds"  (Bool (Set (Set  "("  ($#k6_roughs_1 :::"MemberFunc"::: )   "(" (Set  "("  ($#k1_struct_0 :::"{}"::: )  (Set (Var "A")) ")" ) "," (Set (Var "A")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )))) ; 
 
theorem :: ROUGHS_1:55 (Bool  "for" (Set (Var "A")) "being"   ($#v8_struct_0 :::"finite"::: )    ($#l1_orders_2 :::"Approximation_Space":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A"))  (Bool  "for" (Set (Var "X")) "being"   ($#v1_prob_2 :::"disjoint_valued"::: )     ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "A")))) "holds"  (Bool (Set (Set  "("  ($#k6_roughs_1 :::"MemberFunc"::: )   "(" (Set  "("  ($#k2_roughs_1 :::"Union"::: )  (Set (Var "X")) ")" ) "," (Set (Var "A")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k18_rvsum_1 :::"Sum"::: )  (Set  "("  ($#k7_roughs_1 :::"FinSeqM"::: )   "(" (Set (Var "x")) "," (Set (Var "X")) ")"  ")" )))))) ; 
 
theorem :: ROUGHS_1:56 (Bool  "for" (Set (Var "A")) "being"   ($#v8_struct_0 :::"finite"::: )    ($#l1_orders_2 :::"Approximation_Space":::)  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "holds"  (Bool (Set   ($#k3_roughs_1 :::"LAp"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "x")) where x "is"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) : (Bool (Set (Set  "("  ($#k6_roughs_1 :::"MemberFunc"::: )   "(" (Set (Var "X")) "," (Set (Var "A")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Num 1))  "}"  ))) ; 
 
theorem :: ROUGHS_1:57 (Bool  "for" (Set (Var "A")) "being"   ($#v8_struct_0 :::"finite"::: )    ($#l1_orders_2 :::"Approximation_Space":::)  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "holds"  (Bool (Set   ($#k4_roughs_1 :::"UAp"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "x")) where x "is"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) : (Bool (Set (Set  "("  ($#k6_roughs_1 :::"MemberFunc"::: )   "(" (Set (Var "X")) "," (Set (Var "A")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  "}"  ))) ; 
 
theorem :: ROUGHS_1:58 (Bool  "for" (Set (Var "A")) "being"   ($#v8_struct_0 :::"finite"::: )    ($#l1_orders_2 :::"Approximation_Space":::)  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "holds"  (Bool (Set   ($#k5_roughs_1 :::"BndAp"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "x")) where x "is"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) : (Bool  "("  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Set  "("  ($#k6_roughs_1 :::"MemberFunc"::: )   "(" (Set (Var "X")) "," (Set (Var "A")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))) & (Bool (Set (Set  "("  ($#k6_roughs_1 :::"MemberFunc"::: )   "(" (Set (Var "X")) "," (Set (Var "A")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::"<"::: )  (Num 1))  ")" )  "}"  ))) ; 
 begin  







definitionlet "A" be   ($#l1_orders_2 :::"Tolerance_Space":::); let "X", "Y" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "A")); pred "X" :::"_c="::: "Y" means :: ROUGHS_1:def 11 (Bool (Set   ($#k3_roughs_1 :::"LAp"::: )  "X")  ($#r1_tarski :::"c="::: )  (Set   ($#k3_roughs_1 :::"LAp"::: )  "Y")); reflexivity  
(Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "A")) "holds"  (Bool (Set   ($#k3_roughs_1 :::"LAp"::: )  (Set (Var "X")))  ($#r1_tarski :::"c="::: )  (Set   ($#k3_roughs_1 :::"LAp"::: )  (Set (Var "X")))))
 ; pred "X" :::"c=^"::: "Y" means :: ROUGHS_1:def 12 (Bool (Set   ($#k4_roughs_1 :::"UAp"::: )  "X")  ($#r1_tarski :::"c="::: )  (Set   ($#k4_roughs_1 :::"UAp"::: )  "Y")); reflexivity  
(Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "A")) "holds"  (Bool (Set   ($#k4_roughs_1 :::"UAp"::: )  (Set (Var "X")))  ($#r1_tarski :::"c="::: )  (Set   ($#k4_roughs_1 :::"UAp"::: )  (Set (Var "X")))))
 ; end; 












:: deftheorem    defines :::"_c="::: ROUGHS_1:def 11 :  (Bool  "for" (Set (Var "A")) "being"   ($#l1_orders_2 :::"Tolerance_Space":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "holds"   (Bool  "("  (Bool (Set (Var "X"))  ($#r1_roughs_1 :::"_c="::: )  (Set (Var "Y"))) "iff" (Bool (Set   ($#k3_roughs_1 :::"LAp"::: )  (Set (Var "X")))  ($#r1_tarski :::"c="::: )  (Set   ($#k3_roughs_1 :::"LAp"::: )  (Set (Var "Y"))))  ")" ))); 
 
:: deftheorem    defines :::"c=^"::: ROUGHS_1:def 12 :  (Bool  "for" (Set (Var "A")) "being"   ($#l1_orders_2 :::"Tolerance_Space":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "holds"   (Bool  "("  (Bool (Set (Var "X"))  ($#r2_roughs_1 :::"c=^"::: )  (Set (Var "Y"))) "iff" (Bool (Set   ($#k4_roughs_1 :::"UAp"::: )  (Set (Var "X")))  ($#r1_tarski :::"c="::: )  (Set   ($#k4_roughs_1 :::"UAp"::: )  (Set (Var "Y"))))  ")" ))); 
 definitionlet "A" be   ($#l1_orders_2 :::"Tolerance_Space":::); let "X", "Y" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "A")); pred "X" :::"_c=^"::: "Y" means :: ROUGHS_1:def 13 (Bool  "("  (Bool "X"  ($#r1_roughs_1 :::"_c="::: )  "Y") & (Bool "X"  ($#r2_roughs_1 :::"c=^"::: )  "Y")  ")" ); reflexivity  
(Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "A")) "holds"   (Bool  "("  (Bool (Set (Var "X"))  ($#r1_roughs_1 :::"_c="::: )  (Set (Var "X"))) & (Bool (Set (Var "X"))  ($#r2_roughs_1 :::"c=^"::: )  (Set (Var "X")))  ")" ))
 ; end; 






:: deftheorem    defines :::"_c=^"::: ROUGHS_1:def 13 :  (Bool  "for" (Set (Var "A")) "being"   ($#l1_orders_2 :::"Tolerance_Space":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "holds"   (Bool  "("  (Bool (Set (Var "X"))  ($#r3_roughs_1 :::"_c=^"::: )  (Set (Var "Y"))) "iff" (Bool  "("  (Bool (Set (Var "X"))  ($#r1_roughs_1 :::"_c="::: )  (Set (Var "Y"))) & (Bool (Set (Var "X"))  ($#r2_roughs_1 :::"c=^"::: )  (Set (Var "Y")))  ")" )  ")" ))); 
 
theorem :: ROUGHS_1:59 (Bool  "for" (Set (Var "A")) "being"   ($#l1_orders_2 :::"Tolerance_Space":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A"))  "st" (Bool (Bool (Set (Var "X"))  ($#r1_roughs_1 :::"_c="::: )  (Set (Var "Y"))) & (Bool (Set (Var "Y"))  ($#r1_roughs_1 :::"_c="::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Var "X"))  ($#r1_roughs_1 :::"_c="::: )  (Set (Var "Z"))))) ; 
 
theorem :: ROUGHS_1:60 (Bool  "for" (Set (Var "A")) "being"   ($#l1_orders_2 :::"Tolerance_Space":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A"))  "st" (Bool (Bool (Set (Var "X"))  ($#r2_roughs_1 :::"c=^"::: )  (Set (Var "Y"))) & (Bool (Set (Var "Y"))  ($#r2_roughs_1 :::"c=^"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Var "X"))  ($#r2_roughs_1 :::"c=^"::: )  (Set (Var "Z"))))) ; 
 
theorem :: ROUGHS_1:61 (Bool  "for" (Set (Var "A")) "being"   ($#l1_orders_2 :::"Tolerance_Space":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A"))  "st" (Bool (Bool (Set (Var "X"))  ($#r3_roughs_1 :::"_c=^"::: )  (Set (Var "Y"))) & (Bool (Set (Var "Y"))  ($#r3_roughs_1 :::"_c=^"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Var "X"))  ($#r3_roughs_1 :::"_c=^"::: )  (Set (Var "Z"))))) ; 
 begin  definitionlet "A" be   ($#l1_orders_2 :::"Tolerance_Space":::); let "X", "Y" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "A")); pred "X" :::"_="::: "Y" means :: ROUGHS_1:def 14 (Bool (Set   ($#k3_roughs_1 :::"LAp"::: )  "X")  ($#r1_hidden :::"="::: )  (Set   ($#k3_roughs_1 :::"LAp"::: )  "Y")); reflexivity  
(Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "A")) "holds"  (Bool (Set   ($#k3_roughs_1 :::"LAp"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_roughs_1 :::"LAp"::: )  (Set (Var "X")))))
 ; symmetry  
(Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "A"))  "st" (Bool (Bool (Set   ($#k3_roughs_1 :::"LAp"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_roughs_1 :::"LAp"::: )  (Set (Var "Y"))))) "holds"  (Bool (Set   ($#k3_roughs_1 :::"LAp"::: )  (Set (Var "Y")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_roughs_1 :::"LAp"::: )  (Set (Var "X")))))
 ; pred "X" :::"=^"::: "Y" means :: ROUGHS_1:def 15 (Bool (Set   ($#k4_roughs_1 :::"UAp"::: )  "X")  ($#r1_hidden :::"="::: )  (Set   ($#k4_roughs_1 :::"UAp"::: )  "Y")); reflexivity  
(Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "A")) "holds"  (Bool (Set   ($#k4_roughs_1 :::"UAp"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_roughs_1 :::"UAp"::: )  (Set (Var "X")))))
 ; symmetry  
(Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "A"))  "st" (Bool (Bool (Set   ($#k4_roughs_1 :::"UAp"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_roughs_1 :::"UAp"::: )  (Set (Var "Y"))))) "holds"  (Bool (Set   ($#k4_roughs_1 :::"UAp"::: )  (Set (Var "Y")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_roughs_1 :::"UAp"::: )  (Set (Var "X")))))
 ; pred "X" :::"_=^"::: "Y" means :: ROUGHS_1:def 16 (Bool  "("  (Bool (Set   ($#k3_roughs_1 :::"LAp"::: )  "X")  ($#r1_hidden :::"="::: )  (Set   ($#k3_roughs_1 :::"LAp"::: )  "Y")) & (Bool (Set   ($#k4_roughs_1 :::"UAp"::: )  "X")  ($#r1_hidden :::"="::: )  (Set   ($#k4_roughs_1 :::"UAp"::: )  "Y"))  ")" ); reflexivity  
(Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "A")) "holds"   (Bool  "("  (Bool (Set   ($#k3_roughs_1 :::"LAp"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_roughs_1 :::"LAp"::: )  (Set (Var "X")))) & (Bool (Set   ($#k4_roughs_1 :::"UAp"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_roughs_1 :::"UAp"::: )  (Set (Var "X"))))  ")" ))
 ; symmetry  
(Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "A"))  "st" (Bool (Bool (Set   ($#k3_roughs_1 :::"LAp"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_roughs_1 :::"LAp"::: )  (Set (Var "Y")))) & (Bool (Set   ($#k4_roughs_1 :::"UAp"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_roughs_1 :::"UAp"::: )  (Set (Var "Y"))))) "holds"  (Bool  "("  (Bool (Set   ($#k3_roughs_1 :::"LAp"::: )  (Set (Var "Y")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_roughs_1 :::"LAp"::: )  (Set (Var "X")))) & (Bool (Set   ($#k4_roughs_1 :::"UAp"::: )  (Set (Var "Y")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_roughs_1 :::"UAp"::: )  (Set (Var "X"))))  ")" ))
 ; end; 


















:: deftheorem    defines :::"_="::: ROUGHS_1:def 14 :  (Bool  "for" (Set (Var "A")) "being"   ($#l1_orders_2 :::"Tolerance_Space":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "holds"   (Bool  "("  (Bool (Set (Var "X"))  ($#r4_roughs_1 :::"_="::: )  (Set (Var "Y"))) "iff" (Bool (Set   ($#k3_roughs_1 :::"LAp"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_roughs_1 :::"LAp"::: )  (Set (Var "Y"))))  ")" ))); 
 
:: deftheorem    defines :::"=^"::: ROUGHS_1:def 15 :  (Bool  "for" (Set (Var "A")) "being"   ($#l1_orders_2 :::"Tolerance_Space":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "holds"   (Bool  "("  (Bool (Set (Var "X"))  ($#r5_roughs_1 :::"=^"::: )  (Set (Var "Y"))) "iff" (Bool (Set   ($#k4_roughs_1 :::"UAp"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_roughs_1 :::"UAp"::: )  (Set (Var "Y"))))  ")" ))); 
 
:: deftheorem    defines :::"_=^"::: ROUGHS_1:def 16 :  (Bool  "for" (Set (Var "A")) "being"   ($#l1_orders_2 :::"Tolerance_Space":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "holds"   (Bool  "("  (Bool (Set (Var "X"))  ($#r6_roughs_1 :::"_=^"::: )  (Set (Var "Y"))) "iff" (Bool  "("  (Bool (Set   ($#k3_roughs_1 :::"LAp"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_roughs_1 :::"LAp"::: )  (Set (Var "Y")))) & (Bool (Set   ($#k4_roughs_1 :::"UAp"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_roughs_1 :::"UAp"::: )  (Set (Var "Y"))))  ")" )  ")" ))); 
 definitionlet "A" be   ($#l1_orders_2 :::"Tolerance_Space":::); let "X", "Y" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "A")); redefine pred "X" :::"_="::: "Y" means :: ROUGHS_1:def 17 (Bool  "("  (Bool "X"  ($#r1_roughs_1 :::"_c="::: )  "Y") & (Bool "Y"  ($#r1_roughs_1 :::"_c="::: )  "X")  ")" ); redefine pred "X" :::"=^"::: "Y" means :: ROUGHS_1:def 18 (Bool  "("  (Bool "X"  ($#r2_roughs_1 :::"c=^"::: )  "Y") & (Bool "Y"  ($#r2_roughs_1 :::"c=^"::: )  "X")  ")" ); redefine pred "X" :::"_=^"::: "Y" means :: ROUGHS_1:def 19 (Bool  "("  (Bool "X"  ($#r4_roughs_1 :::"_="::: )  "Y") & (Bool "X"  ($#r5_roughs_1 :::"=^"::: )  "Y")  ")" ); end; 


















:: deftheorem    defines :::"_="::: ROUGHS_1:def 17 :  (Bool  "for" (Set (Var "A")) "being"   ($#l1_orders_2 :::"Tolerance_Space":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "holds"   (Bool  "("  (Bool (Set (Var "X"))  ($#r4_roughs_1 :::"_="::: )  (Set (Var "Y"))) "iff" (Bool  "("  (Bool (Set (Var "X"))  ($#r1_roughs_1 :::"_c="::: )  (Set (Var "Y"))) & (Bool (Set (Var "Y"))  ($#r1_roughs_1 :::"_c="::: )  (Set (Var "X")))  ")" )  ")" ))); 
 
:: deftheorem    defines :::"=^"::: ROUGHS_1:def 18 :  (Bool  "for" (Set (Var "A")) "being"   ($#l1_orders_2 :::"Tolerance_Space":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "holds"   (Bool  "("  (Bool (Set (Var "X"))  ($#r5_roughs_1 :::"=^"::: )  (Set (Var "Y"))) "iff" (Bool  "("  (Bool (Set (Var "X"))  ($#r2_roughs_1 :::"c=^"::: )  (Set (Var "Y"))) & (Bool (Set (Var "Y"))  ($#r2_roughs_1 :::"c=^"::: )  (Set (Var "X")))  ")" )  ")" ))); 
 
:: deftheorem    defines :::"_=^"::: ROUGHS_1:def 19 :  (Bool  "for" (Set (Var "A")) "being"   ($#l1_orders_2 :::"Tolerance_Space":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "holds"   (Bool  "("  (Bool (Set (Var "X"))  ($#r6_roughs_1 :::"_=^"::: )  (Set (Var "Y"))) "iff" (Bool  "("  (Bool (Set (Var "X"))  ($#r4_roughs_1 :::"_="::: )  (Set (Var "Y"))) & (Bool (Set (Var "X"))  ($#r5_roughs_1 :::"=^"::: )  (Set (Var "Y")))  ")" )  ")" )));