:: GOBRD11  semantic presentation begin  





















theorem :: GOBRD11:1 (Bool  "for" (Set (Var "GX")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX"))  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "GX"))  "st" (Bool (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool (Set (Var "A")) "is"   ($#v2_connsp_1 :::"connected"::: )  )) "holds"  (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_connsp_1 :::"Component_of"::: )  (Set (Var "p"))))))) ; 
 
theorem :: GOBRD11:2 (Bool  "for" (Set (Var "GX")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX"))  "st" (Bool (Bool (Set (Var "C")) "is"   ($#v3_connsp_1 :::"a_component"::: )  ) & (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Var "C"))) & (Bool (Set (Var "B")) "is"   ($#v2_connsp_1 :::"connected"::: )  ) & (Bool (Set   ($#k2_pre_topc :::"Cl"::: )  (Set (Var "A")))  ($#r1_xboole_0 :::"meets"::: )  (Set   ($#k2_pre_topc :::"Cl"::: )  (Set (Var "B"))))) "holds"  (Bool (Set (Var "B"))  ($#r1_tarski :::"c="::: )  (Set (Var "C"))))) ; 
 



theorem :: GOBRD11:3 (Bool  "for" (Set (Var "GZ")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GZ"))  "st" (Bool (Bool (Set (Var "A")) "is"   ($#v3_connsp_1 :::"a_component"::: )  ) & (Bool (Set (Var "B")) "is"   ($#v3_connsp_1 :::"a_component"::: )  )) "holds"  (Bool (Set (Set (Var "A"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "B"))) "is"    ($#m1_connsp_3 :::"a_union_of_components"::: )   "of" (Set (Var "GZ"))))) ; 
 
theorem :: GOBRD11:4 (Bool  "for" (Set (Var "GX")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "B1")) "," (Set (Var "B2")) "," (Set (Var "V")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "holds"  (Bool (Set   ($#k4_connsp_3 :::"Down"::: )   "(" (Set  "(" (Set (Var "B1"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "B2")) ")" ) "," (Set (Var "V")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_connsp_3 :::"Down"::: )   "(" (Set (Var "B1")) "," (Set (Var "V")) ")"  ")" )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k4_connsp_3 :::"Down"::: )   "(" (Set (Var "B2")) "," (Set (Var "V")) ")"  ")" ))))) ; 
 
theorem :: GOBRD11:5 (Bool  "for" (Set (Var "GX")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "B1")) "," (Set (Var "B2")) "," (Set (Var "V")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "holds"  (Bool (Set   ($#k4_connsp_3 :::"Down"::: )   "(" (Set  "(" (Set (Var "B1"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "B2")) ")" ) "," (Set (Var "V")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_connsp_3 :::"Down"::: )   "(" (Set (Var "B1")) "," (Set (Var "V")) ")"  ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k4_connsp_3 :::"Down"::: )   "(" (Set (Var "B2")) "," (Set (Var "V")) ")"  ")" ))))) ; 
 






theorem :: GOBRD11:6 (Bool  "for" (Set (Var "f")) "being"  ($#~v3_funct_1  "non"   ($#v3_funct_1 :::"constant"::: )   )    ($#v2_goboard5 :::"standard"::: )    ($#m2_finseq_1 :::"special_circular_sequence":::)  "holds" (Bool (Set (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" )  ($#k3_subset_1 :::"`"::: )  )  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) ; 
 registrationlet "f" be  ($#~v3_funct_1  "non"   ($#v3_funct_1 :::"constant"::: )   )    ($#v2_goboard5 :::"standard"::: )    ($#m2_finseq_1 :::"special_circular_sequence":::); 
cluster (Set (Set  "("  ($#k3_topreal1 :::"L~"::: )  "f" ")" )  ($#k3_subset_1 :::"`"::: )  ) ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; 
theorem :: GOBRD11:7 (Bool  "for" (Set (Var "f")) "being"  ($#~v3_funct_1  "non"   ($#v3_funct_1 :::"constant"::: )   )    ($#v2_goboard5 :::"standard"::: )    ($#m2_finseq_1 :::"special_circular_sequence":::) "holds"  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k3_tarski :::"union"::: )   "{"  (Set  "("  ($#k3_goboard5 :::"cell"::: )   "(" (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ) "," (Set (Var "i")) "," (Set (Var "j")) ")"  ")" ) where i, j "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) : (Bool  "("  (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" ))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set  "("  ($#k2_goboard2 :::"GoB"::: )  (Set (Var "f")) ")" )))  ")" )  "}"  ))) ; 
 
theorem :: GOBRD11:8 (Bool  "for" (Set (Var "s1")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "P1")) "," (Set (Var "P2")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "P1"))  ($#r1_hidden :::"="::: )   "{"  (Set  ($#k19_euclid :::"|["::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k19_euclid :::"]|"::: ) ) where r, s "is"   ($#m1_subset_1 :::"Real":::) : (Bool (Set (Var "s"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s1")))  "}"  ) & (Bool (Set (Var "P2"))  ($#r1_hidden :::"="::: )   "{"  (Set  ($#k19_euclid :::"|["::: ) (Set (Var "r2")) "," (Set (Var "s2")) ($#k19_euclid :::"]|"::: ) ) where r2, s2 "is"   ($#m1_subset_1 :::"Real":::) : (Bool (Set (Var "s2"))  ($#r1_xxreal_0 :::">"::: )  (Set (Var "s1")))  "}"  )) "holds"  (Bool (Set (Var "P1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "P2"))  ($#k3_subset_1 :::"`"::: )  )))) ; 
 
theorem :: GOBRD11:9 (Bool  "for" (Set (Var "s1")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "P1")) "," (Set (Var "P2")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "P1"))  ($#r1_hidden :::"="::: )   "{"  (Set  ($#k19_euclid :::"|["::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k19_euclid :::"]|"::: ) ) where r, s "is"   ($#m1_subset_1 :::"Real":::) : (Bool (Set (Var "s"))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "s1")))  "}"  ) & (Bool (Set (Var "P2"))  ($#r1_hidden :::"="::: )   "{"  (Set  ($#k19_euclid :::"|["::: ) (Set (Var "r2")) "," (Set (Var "s2")) ($#k19_euclid :::"]|"::: ) ) where r2, s2 "is"   ($#m1_subset_1 :::"Real":::) : (Bool (Set (Var "s2"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "s1")))  "}"  )) "holds"  (Bool (Set (Var "P1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "P2"))  ($#k3_subset_1 :::"`"::: )  )))) ; 
 
theorem :: GOBRD11:10 (Bool  "for" (Set (Var "s1")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "P1")) "," (Set (Var "P2")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "P1"))  ($#r1_hidden :::"="::: )   "{"  (Set  ($#k19_euclid :::"|["::: ) (Set (Var "s")) "," (Set (Var "r")) ($#k19_euclid :::"]|"::: ) ) where s, r "is"   ($#m1_subset_1 :::"Real":::) : (Bool (Set (Var "s"))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "s1")))  "}"  ) & (Bool (Set (Var "P2"))  ($#r1_hidden :::"="::: )   "{"  (Set  ($#k19_euclid :::"|["::: ) (Set (Var "s2")) "," (Set (Var "r2")) ($#k19_euclid :::"]|"::: ) ) where s2, r2 "is"   ($#m1_subset_1 :::"Real":::) : (Bool (Set (Var "s2"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "s1")))  "}"  )) "holds"  (Bool (Set (Var "P1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "P2"))  ($#k3_subset_1 :::"`"::: )  )))) ; 
 
theorem :: GOBRD11:11 (Bool  "for" (Set (Var "s1")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "P1")) "," (Set (Var "P2")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "P1"))  ($#r1_hidden :::"="::: )   "{"  (Set  ($#k19_euclid :::"|["::: ) (Set (Var "s")) "," (Set (Var "r")) ($#k19_euclid :::"]|"::: ) ) where s, r "is"   ($#m1_subset_1 :::"Real":::) : (Bool (Set (Var "s"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s1")))  "}"  ) & (Bool (Set (Var "P2"))  ($#r1_hidden :::"="::: )   "{"  (Set  ($#k19_euclid :::"|["::: ) (Set (Var "s2")) "," (Set (Var "r2")) ($#k19_euclid :::"]|"::: ) ) where s2, r2 "is"   ($#m1_subset_1 :::"Real":::) : (Bool (Set (Var "s2"))  ($#r1_xxreal_0 :::">"::: )  (Set (Var "s1")))  "}"  )) "holds"  (Bool (Set (Var "P1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "P2"))  ($#k3_subset_1 :::"`"::: )  )))) ; 
 
theorem :: GOBRD11:12 (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "s1")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "P"))  ($#r1_hidden :::"="::: )   "{"  (Set  ($#k19_euclid :::"|["::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k19_euclid :::"]|"::: ) ) where r, s "is"   ($#m1_subset_1 :::"Real":::) : (Bool (Set (Var "s"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s1")))  "}"  )) "holds"  (Bool (Set (Var "P")) "is"   ($#v4_pre_topc :::"closed"::: )  ))) ; 
 
theorem :: GOBRD11:13 (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "s1")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "P"))  ($#r1_hidden :::"="::: )   "{"  (Set  ($#k19_euclid :::"|["::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k19_euclid :::"]|"::: ) ) where r, s "is"   ($#m1_subset_1 :::"Real":::) : (Bool (Set (Var "s1"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s")))  "}"  )) "holds"  (Bool (Set (Var "P")) "is"   ($#v4_pre_topc :::"closed"::: )  ))) ; 
 
theorem :: GOBRD11:14 (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "s1")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "P"))  ($#r1_hidden :::"="::: )   "{"  (Set  ($#k19_euclid :::"|["::: ) (Set (Var "s")) "," (Set (Var "r")) ($#k19_euclid :::"]|"::: ) ) where s, r "is"   ($#m1_subset_1 :::"Real":::) : (Bool (Set (Var "s"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s1")))  "}"  )) "holds"  (Bool (Set (Var "P")) "is"   ($#v4_pre_topc :::"closed"::: )  ))) ; 
 
theorem :: GOBRD11:15 (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "s1")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "P"))  ($#r1_hidden :::"="::: )   "{"  (Set  ($#k19_euclid :::"|["::: ) (Set (Var "s")) "," (Set (Var "r")) ($#k19_euclid :::"]|"::: ) ) where s, r "is"   ($#m1_subset_1 :::"Real":::) : (Bool (Set (Var "s1"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s")))  "}"  )) "holds"  (Bool (Set (Var "P")) "is"   ($#v4_pre_topc :::"closed"::: )  ))) ; 
 
theorem :: GOBRD11:16 (Bool  "for" (Set (Var "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "G")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set   ($#k2_goboard5 :::"h_strip"::: )   "(" (Set (Var "G")) "," (Set (Var "j")) ")" ) "is"   ($#v4_pre_topc :::"closed"::: )  ))) ; 
 
theorem :: GOBRD11:17 (Bool  "for" (Set (Var "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "G")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set   ($#k1_goboard5 :::"v_strip"::: )   "(" (Set (Var "G")) "," (Set (Var "j")) ")" ) "is"   ($#v4_pre_topc :::"closed"::: )  ))) ; 
 
theorem :: GOBRD11:18 (Bool  "for" (Set (Var "G")) "being" bbbadV3_RELAT_1()  ($#m2_finseq_1 :::"Matrix":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "G")) "is"   ($#v2_goboard1 :::"X_equal-in-line"::: )  )) "holds"  (Bool (Set   ($#k1_goboard5 :::"v_strip"::: )   "(" (Set (Var "G")) "," (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#r1_hidden :::"="::: )   "{"  (Set  ($#k19_euclid :::"|["::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k19_euclid :::"]|"::: ) ) where r, s "is"   ($#m1_subset_1 :::"Real":::) : (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Num 1) "," (Num 1) ")"  ")" )  ($#k17_euclid :::"`1"::: )  ))  "}"  )) ; 
 
theorem :: GOBRD11:19 (Bool  "for" (Set (Var "G")) "being" bbbadV3_RELAT_1()  ($#m2_finseq_1 :::"Matrix":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "G")) "is"   ($#v2_goboard1 :::"X_equal-in-line"::: )  )) "holds"  (Bool (Set   ($#k1_goboard5 :::"v_strip"::: )   "(" (Set (Var "G")) "," (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "G")) ")" ) ")" )  ($#r1_hidden :::"="::: )   "{"  (Set  ($#k19_euclid :::"|["::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k19_euclid :::"]|"::: ) ) where r, s "is"   ($#m1_subset_1 :::"Real":::) : (Bool (Set (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "G")) ")" ) "," (Num 1) ")"  ")" )  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "r")))  "}"  )) ; 
 
theorem :: GOBRD11:20 (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "G")) "being" bbbadV3_RELAT_1()  ($#m2_finseq_1 :::"Matrix":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "G")) "is"   ($#v2_goboard1 :::"X_equal-in-line"::: )  ) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "G"))))) "holds"  (Bool (Set   ($#k1_goboard5 :::"v_strip"::: )   "(" (Set (Var "G")) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )   "{"  (Set  ($#k19_euclid :::"|["::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k19_euclid :::"]|"::: ) ) where r, s "is"   ($#m1_subset_1 :::"Real":::) : (Bool  "("  (Bool (Set (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Num 1) ")"  ")" )  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "r"))) & (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) "," (Num 1) ")"  ")" )  ($#k17_euclid :::"`1"::: )  ))  ")" )  "}"  ))) ; 
 
theorem :: GOBRD11:21 (Bool  "for" (Set (Var "G")) "being" bbbadV3_RELAT_1()  ($#m2_finseq_1 :::"Matrix":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "G")) "is"   ($#v3_goboard1 :::"Y_equal-in-column"::: )  )) "holds"  (Bool (Set   ($#k2_goboard5 :::"h_strip"::: )   "(" (Set (Var "G")) "," (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#r1_hidden :::"="::: )   "{"  (Set  ($#k19_euclid :::"|["::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k19_euclid :::"]|"::: ) ) where r, s "is"   ($#m1_subset_1 :::"Real":::) : (Bool (Set (Var "s"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Num 1) "," (Num 1) ")"  ")" )  ($#k18_euclid :::"`2"::: )  ))  "}"  )) ; 
 
theorem :: GOBRD11:22 (Bool  "for" (Set (Var "G")) "being" bbbadV3_RELAT_1()  ($#m2_finseq_1 :::"Matrix":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "G")) "is"   ($#v3_goboard1 :::"Y_equal-in-column"::: )  )) "holds"  (Bool (Set   ($#k2_goboard5 :::"h_strip"::: )   "(" (Set (Var "G")) "," (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")) ")" ) ")" )  ($#r1_hidden :::"="::: )   "{"  (Set  ($#k19_euclid :::"|["::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k19_euclid :::"]|"::: ) ) where r, s "is"   ($#m1_subset_1 :::"Real":::) : (Bool (Set (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Num 1) "," (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")) ")" ) ")"  ")" )  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s")))  "}"  )) ; 
 
theorem :: GOBRD11:23 (Bool  "for" (Set (Var "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "G")) "being" bbbadV3_RELAT_1()  ($#m2_finseq_1 :::"Matrix":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "G")) "is"   ($#v3_goboard1 :::"Y_equal-in-column"::: )  ) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "j"))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "G"))))) "holds"  (Bool (Set   ($#k2_goboard5 :::"h_strip"::: )   "(" (Set (Var "G")) "," (Set (Var "j")) ")" )  ($#r1_hidden :::"="::: )   "{"  (Set  ($#k19_euclid :::"|["::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k19_euclid :::"]|"::: ) ) where r, s "is"   ($#m1_subset_1 :::"Real":::) : (Bool  "("  (Bool (Set (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Num 1) "," (Set (Var "j")) ")"  ")" )  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s"))) & (Bool (Set (Var "s"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Num 1) "," (Set  "(" (Set (Var "j"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")"  ")" )  ($#k18_euclid :::"`2"::: )  ))  ")" )  "}"  ))) ; 
 



theorem :: GOBRD11:24 (Bool  "for" (Set (Var "G")) "being" bbbadV3_RELAT_1()   ($#v2_goboard1 :::"X_equal-in-line"::: )     ($#v3_goboard1 :::"Y_equal-in-column"::: )    ($#m2_finseq_1 :::"Matrix":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set   ($#k3_goboard5 :::"cell"::: )   "(" (Set (Var "G")) "," (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#r1_hidden :::"="::: )   "{"  (Set  ($#k19_euclid :::"|["::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k19_euclid :::"]|"::: ) ) where r, s "is"   ($#m1_subset_1 :::"Real":::) : (Bool  "("  (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Num 1) "," (Num 1) ")"  ")" )  ($#k17_euclid :::"`1"::: )  )) & (Bool (Set (Var "s"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Num 1) "," (Num 1) ")"  ")" )  ($#k18_euclid :::"`2"::: )  ))  ")" )  "}"  )) ; 
 
theorem :: GOBRD11:25 (Bool  "for" (Set (Var "G")) "being" bbbadV3_RELAT_1()   ($#v2_goboard1 :::"X_equal-in-line"::: )     ($#v3_goboard1 :::"Y_equal-in-column"::: )    ($#m2_finseq_1 :::"Matrix":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set   ($#k3_goboard5 :::"cell"::: )   "(" (Set (Var "G")) "," (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")) ")" ) ")" )  ($#r1_hidden :::"="::: )   "{"  (Set  ($#k19_euclid :::"|["::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k19_euclid :::"]|"::: ) ) where r, s "is"   ($#m1_subset_1 :::"Real":::) : (Bool  "("  (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Num 1) "," (Num 1) ")"  ")" )  ($#k17_euclid :::"`1"::: )  )) & (Bool (Set (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Num 1) "," (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")) ")" ) ")"  ")" )  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s")))  ")" )  "}"  )) ; 
 
theorem :: GOBRD11:26 (Bool  "for" (Set (Var "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "G")) "being" bbbadV3_RELAT_1()   ($#v2_goboard1 :::"X_equal-in-line"::: )     ($#v3_goboard1 :::"Y_equal-in-column"::: )    ($#m2_finseq_1 :::"Matrix":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "j"))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "G"))))) "holds"  (Bool (Set   ($#k3_goboard5 :::"cell"::: )   "(" (Set (Var "G")) "," (Set  ($#k6_numbers :::"0"::: ) ) "," (Set (Var "j")) ")" )  ($#r1_hidden :::"="::: )   "{"  (Set  ($#k19_euclid :::"|["::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k19_euclid :::"]|"::: ) ) where r, s "is"   ($#m1_subset_1 :::"Real":::) : (Bool  "("  (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Num 1) "," (Num 1) ")"  ")" )  ($#k17_euclid :::"`1"::: )  )) & (Bool (Set (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Num 1) "," (Set (Var "j")) ")"  ")" )  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s"))) & (Bool (Set (Var "s"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Num 1) "," (Set  "(" (Set (Var "j"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")"  ")" )  ($#k18_euclid :::"`2"::: )  ))  ")" )  "}"  ))) ; 
 
theorem :: GOBRD11:27 (Bool  "for" (Set (Var "G")) "being" bbbadV3_RELAT_1()   ($#v2_goboard1 :::"X_equal-in-line"::: )     ($#v3_goboard1 :::"Y_equal-in-column"::: )    ($#m2_finseq_1 :::"Matrix":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set   ($#k3_goboard5 :::"cell"::: )   "(" (Set (Var "G")) "," (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "G")) ")" ) "," (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#r1_hidden :::"="::: )   "{"  (Set  ($#k19_euclid :::"|["::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k19_euclid :::"]|"::: ) ) where r, s "is"   ($#m1_subset_1 :::"Real":::) : (Bool  "("  (Bool (Set (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "G")) ")" ) "," (Num 1) ")"  ")" )  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "r"))) & (Bool (Set (Var "s"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Num 1) "," (Num 1) ")"  ")" )  ($#k18_euclid :::"`2"::: )  ))  ")" )  "}"  )) ; 
 
theorem :: GOBRD11:28 (Bool  "for" (Set (Var "G")) "being" bbbadV3_RELAT_1()   ($#v2_goboard1 :::"X_equal-in-line"::: )     ($#v3_goboard1 :::"Y_equal-in-column"::: )    ($#m2_finseq_1 :::"Matrix":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set   ($#k3_goboard5 :::"cell"::: )   "(" (Set (Var "G")) "," (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "G")) ")" ) "," (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")) ")" ) ")" )  ($#r1_hidden :::"="::: )   "{"  (Set  ($#k19_euclid :::"|["::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k19_euclid :::"]|"::: ) ) where r, s "is"   ($#m1_subset_1 :::"Real":::) : (Bool  "("  (Bool (Set (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "G")) ")" ) "," (Num 1) ")"  ")" )  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "r"))) & (Bool (Set (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Num 1) "," (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")) ")" ) ")"  ")" )  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s")))  ")" )  "}"  )) ; 
 
theorem :: GOBRD11:29 (Bool  "for" (Set (Var "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "G")) "being" bbbadV3_RELAT_1()   ($#v2_goboard1 :::"X_equal-in-line"::: )     ($#v3_goboard1 :::"Y_equal-in-column"::: )    ($#m2_finseq_1 :::"Matrix":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "j"))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "G"))))) "holds"  (Bool (Set   ($#k3_goboard5 :::"cell"::: )   "(" (Set (Var "G")) "," (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "G")) ")" ) "," (Set (Var "j")) ")" )  ($#r1_hidden :::"="::: )   "{"  (Set  ($#k19_euclid :::"|["::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k19_euclid :::"]|"::: ) ) where r, s "is"   ($#m1_subset_1 :::"Real":::) : (Bool  "("  (Bool (Set (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "G")) ")" ) "," (Num 1) ")"  ")" )  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "r"))) & (Bool (Set (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Num 1) "," (Set (Var "j")) ")"  ")" )  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s"))) & (Bool (Set (Var "s"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Num 1) "," (Set  "(" (Set (Var "j"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")"  ")" )  ($#k18_euclid :::"`2"::: )  ))  ")" )  "}"  ))) ; 
 
theorem :: GOBRD11:30 (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "G")) "being" bbbadV3_RELAT_1()   ($#v2_goboard1 :::"X_equal-in-line"::: )     ($#v3_goboard1 :::"Y_equal-in-column"::: )    ($#m2_finseq_1 :::"Matrix":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "G"))))) "holds"  (Bool (Set   ($#k3_goboard5 :::"cell"::: )   "(" (Set (Var "G")) "," (Set (Var "i")) "," (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#r1_hidden :::"="::: )   "{"  (Set  ($#k19_euclid :::"|["::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k19_euclid :::"]|"::: ) ) where r, s "is"   ($#m1_subset_1 :::"Real":::) : (Bool  "("  (Bool (Set (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Num 1) ")"  ")" )  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "r"))) & (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) "," (Num 1) ")"  ")" )  ($#k17_euclid :::"`1"::: )  )) & (Bool (Set (Var "s"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Num 1) "," (Num 1) ")"  ")" )  ($#k18_euclid :::"`2"::: )  ))  ")" )  "}"  ))) ; 
 
theorem :: GOBRD11:31 (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "G")) "being" bbbadV3_RELAT_1()   ($#v2_goboard1 :::"X_equal-in-line"::: )     ($#v3_goboard1 :::"Y_equal-in-column"::: )    ($#m2_finseq_1 :::"Matrix":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "G"))))) "holds"  (Bool (Set   ($#k3_goboard5 :::"cell"::: )   "(" (Set (Var "G")) "," (Set (Var "i")) "," (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")) ")" ) ")" )  ($#r1_hidden :::"="::: )   "{"  (Set  ($#k19_euclid :::"|["::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k19_euclid :::"]|"::: ) ) where r, s "is"   ($#m1_subset_1 :::"Real":::) : (Bool  "("  (Bool (Set (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Num 1) ")"  ")" )  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "r"))) & (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) "," (Num 1) ")"  ")" )  ($#k17_euclid :::"`1"::: )  )) & (Bool (Set (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Num 1) "," (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "G")) ")" ) ")"  ")" )  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s")))  ")" )  "}"  ))) ; 
 
theorem :: GOBRD11:32 (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "G")) "being" bbbadV3_RELAT_1()   ($#v2_goboard1 :::"X_equal-in-line"::: )     ($#v3_goboard1 :::"Y_equal-in-column"::: )    ($#m2_finseq_1 :::"Matrix":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "G")))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "j"))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "G"))))) "holds"  (Bool (Set   ($#k3_goboard5 :::"cell"::: )   "(" (Set (Var "G")) "," (Set (Var "i")) "," (Set (Var "j")) ")" )  ($#r1_hidden :::"="::: )   "{"  (Set  ($#k19_euclid :::"|["::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k19_euclid :::"]|"::: ) ) where r, s "is"   ($#m1_subset_1 :::"Real":::) : (Bool  "("  (Bool (Set (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Num 1) ")"  ")" )  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "r"))) & (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) "," (Num 1) ")"  ")" )  ($#k17_euclid :::"`1"::: )  )) & (Bool (Set (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Num 1) "," (Set (Var "j")) ")"  ")" )  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s"))) & (Bool (Set (Var "s"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Num 1) "," (Set  "(" (Set (Var "j"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")"  ")" )  ($#k18_euclid :::"`2"::: )  ))  ")" )  "}"  ))) ; 
 
theorem :: GOBRD11:33 (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "G")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set   ($#k3_goboard5 :::"cell"::: )   "(" (Set (Var "G")) "," (Set (Var "i")) "," (Set (Var "j")) ")" ) "is"   ($#v4_pre_topc :::"closed"::: )  ))) ; 
 
theorem :: GOBRD11:34 (Bool  "for" (Set (Var "G")) "being" bbbadV3_RELAT_1()  ($#m2_finseq_1 :::"Matrix":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"   (Bool  "("  (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "G")))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "G"))))  ")" )) ; 
 
theorem :: GOBRD11:35 (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "G")) "being"   ($#m2_finseq_1 :::"Go-board":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "G")))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "G"))))) "holds"  (Bool (Set   ($#k3_goboard5 :::"cell"::: )   "(" (Set (Var "G")) "," (Set (Var "i")) "," (Set (Var "j")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k2_pre_topc :::"Cl"::: )  (Set  "("  ($#k1_tops_1 :::"Int"::: )  (Set  "("  ($#k3_goboard5 :::"cell"::: )   "(" (Set (Var "G")) "," (Set (Var "i")) "," (Set (Var "j")) ")"  ")" ) ")" ))))) ;