:: MATROID0 semantic presentation begin notationlet "x", "y" be ($#m1_hidden :::"set"::: ) ; antonym "x" :::"c/="::: "y" for "x" :::"c="::: "y"; end; definitionmode SubsetFamilyStr is ($#l1_pre_topc :::"TopStruct"::: ) ; end; notationlet "M" be ($#l1_pre_topc :::"SubsetFamilyStr":::); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "M")); synonym :::"independent"::: "A" for :::"open"::: ; antonym :::"dependent"::: "A" for :::"open"::: ; end; definitionlet "M" be ($#l1_pre_topc :::"SubsetFamilyStr":::); func :::"the_family_of"::: "M" -> ($#m1_subset_1 :::"Subset-Family":::) "of" "M" equals :: MATROID0:def 1 (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" "M"); end; :: deftheorem defines :::"the_family_of"::: MATROID0:def 1 : (Bool "for" (Set (Var "M")) "being" ($#l1_pre_topc :::"SubsetFamilyStr":::) "holds" (Bool (Set ($#k1_matroid0 :::"the_family_of"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "M"))))); definitionlet "M" be ($#l1_pre_topc :::"SubsetFamilyStr":::); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "M")); redefine attr "A" is :::"open"::: means :: MATROID0:def 2 (Bool "A" ($#r2_hidden :::"in"::: ) (Set ($#k1_matroid0 :::"the_family_of"::: ) "M")); end; :: deftheorem defines :::"independent"::: MATROID0:def 2 : (Bool "for" (Set (Var "M")) "being" ($#l1_pre_topc :::"SubsetFamilyStr":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"independent"::: ) ) "iff" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set ($#k1_matroid0 :::"the_family_of"::: ) (Set (Var "M")))) ")" ))); definitionlet "M" be ($#l1_pre_topc :::"SubsetFamilyStr":::); attr "M" is :::"subset-closed"::: means :: MATROID0:def 3 (Bool (Set ($#k1_matroid0 :::"the_family_of"::: ) "M") "is" ($#v1_classes1 :::"subset-closed"::: ) ); attr "M" is :::"with_exchange_property"::: means :: MATROID0:def 4 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" "M" "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set ($#k1_matroid0 :::"the_family_of"::: ) "M")) & (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set ($#k1_matroid0 :::"the_family_of"::: ) "M")) & (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "A")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1)))) "holds" (Bool "ex" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element":::) "of" "M" "st" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "B")) ($#k7_subset_1 :::"\"::: ) (Set (Var "A")))) & (Bool (Set (Set (Var "A")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "e")) ($#k1_tarski :::"}"::: ) )) ($#r2_hidden :::"in"::: ) (Set ($#k1_matroid0 :::"the_family_of"::: ) "M")) ")" ))); end; :: deftheorem defines :::"subset-closed"::: MATROID0:def 3 : (Bool "for" (Set (Var "M")) "being" ($#l1_pre_topc :::"SubsetFamilyStr":::) "holds" (Bool "(" (Bool (Set (Var "M")) "is" ($#v1_matroid0 :::"subset-closed"::: ) ) "iff" (Bool (Set ($#k1_matroid0 :::"the_family_of"::: ) (Set (Var "M"))) "is" ($#v1_classes1 :::"subset-closed"::: ) ) ")" )); :: deftheorem defines :::"with_exchange_property"::: MATROID0:def 4 : (Bool "for" (Set (Var "M")) "being" ($#l1_pre_topc :::"SubsetFamilyStr":::) "holds" (Bool "(" (Bool (Set (Var "M")) "is" ($#v2_matroid0 :::"with_exchange_property"::: ) ) "iff" (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set ($#k1_matroid0 :::"the_family_of"::: ) (Set (Var "M")))) & (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set ($#k1_matroid0 :::"the_family_of"::: ) (Set (Var "M")))) & (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "A")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1)))) "holds" (Bool "ex" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "B")) ($#k7_subset_1 :::"\"::: ) (Set (Var "A")))) & (Bool (Set (Set (Var "A")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "e")) ($#k1_tarski :::"}"::: ) )) ($#r2_hidden :::"in"::: ) (Set ($#k1_matroid0 :::"the_family_of"::: ) (Set (Var "M")))) ")" ))) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#v1_pre_topc :::"strict"::: ) ($#~v3_pencil_1 "non" ($#v3_pencil_1 :::"void"::: ) ) ($#v1_matroid0 :::"subset-closed"::: ) ($#v2_matroid0 :::"with_exchange_property"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; end; registrationlet "M" be ($#~v3_pencil_1 "non" ($#v3_pencil_1 :::"void"::: ) ) ($#l1_pre_topc :::"SubsetFamilyStr":::); cluster ($#v3_pre_topc :::"independent"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M"))); end; registrationlet "M" be ($#v1_matroid0 :::"subset-closed"::: ) ($#l1_pre_topc :::"SubsetFamilyStr":::); cluster (Set ($#k1_matroid0 :::"the_family_of"::: ) "M") -> ($#v1_classes1 :::"subset-closed"::: ) ; end; theorem :: MATROID0:1 (Bool "for" (Set (Var "M")) "being" ($#~v3_pencil_1 "non" ($#v3_pencil_1 :::"void"::: ) ) ($#v1_matroid0 :::"subset-closed"::: ) ($#l1_pre_topc :::"SubsetFamilyStr":::) (Bool "for" (Set (Var "A")) "being" ($#v3_pre_topc :::"independent"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "B")) "is" ($#v3_pre_topc :::"independent"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")))))) ; registrationlet "M" be ($#~v3_pencil_1 "non" ($#v3_pencil_1 :::"void"::: ) ) ($#v1_matroid0 :::"subset-closed"::: ) ($#l1_pre_topc :::"SubsetFamilyStr":::); cluster ($#v1_finset_1 :::"finite"::: ) ($#v3_pre_topc :::"independent"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M"))); end; definitionmode Matroid is ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v3_pencil_1 "non" ($#v3_pencil_1 :::"void"::: ) ) ($#v1_matroid0 :::"subset-closed"::: ) ($#v2_matroid0 :::"with_exchange_property"::: ) ($#l1_pre_topc :::"SubsetFamilyStr":::); end; theorem :: MATROID0:2 (Bool "for" (Set (Var "M")) "being" ($#v1_matroid0 :::"subset-closed"::: ) ($#l1_pre_topc :::"SubsetFamilyStr":::) "holds" (Bool "(" (Bool (Bool "not" (Set (Var "M")) "is" ($#v3_pencil_1 :::"void"::: ) )) "iff" (Bool (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_matroid0 :::"the_family_of"::: ) (Set (Var "M")))) ")" )) ; registrationlet "M" be ($#~v3_pencil_1 "non" ($#v3_pencil_1 :::"void"::: ) ) ($#v1_matroid0 :::"subset-closed"::: ) ($#l1_pre_topc :::"SubsetFamilyStr":::); cluster ($#v1_xboole_0 :::"empty"::: ) -> ($#v3_pre_topc :::"independent"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M"))); end; theorem :: MATROID0:3 (Bool "for" (Set (Var "M")) "being" ($#~v3_pencil_1 "non" ($#v3_pencil_1 :::"void"::: ) ) ($#l1_pre_topc :::"SubsetFamilyStr":::) "holds" (Bool "(" (Bool (Set (Var "M")) "is" ($#v1_matroid0 :::"subset-closed"::: ) ) "iff" (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"independent"::: ) ) & (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "B")) "is" ($#v3_pre_topc :::"independent"::: ) )) ")" )) ; registrationlet "M" be ($#~v3_pencil_1 "non" ($#v3_pencil_1 :::"void"::: ) ) ($#v1_matroid0 :::"subset-closed"::: ) ($#l1_pre_topc :::"SubsetFamilyStr":::); let "A" be ($#v3_pre_topc :::"independent"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "M")); let "B" be ($#m1_hidden :::"set"::: ) ; cluster (Set "A" ($#k3_xboole_0 :::"/\"::: ) "B") -> ($#v3_pre_topc :::"independent"::: ) for ($#m1_subset_1 :::"Subset":::) "of" "M"; cluster (Set "B" ($#k3_xboole_0 :::"/\"::: ) "A") -> ($#v3_pre_topc :::"independent"::: ) for ($#m1_subset_1 :::"Subset":::) "of" "M"; cluster (Set "A" ($#k4_xboole_0 :::"\"::: ) "B") -> ($#v3_pre_topc :::"independent"::: ) for ($#m1_subset_1 :::"Subset":::) "of" "M"; end; theorem :: MATROID0:4 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v3_pencil_1 "non" ($#v3_pencil_1 :::"void"::: ) ) ($#l1_pre_topc :::"SubsetFamilyStr":::) "holds" (Bool "(" (Bool (Set (Var "M")) "is" ($#v2_matroid0 :::"with_exchange_property"::: ) ) "iff" (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"independent"::: ) ) & (Bool (Set (Var "B")) "is" ($#v3_pre_topc :::"independent"::: ) ) & (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "A")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1)))) "holds" (Bool "ex" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "B")) ($#k7_subset_1 :::"\"::: ) (Set (Var "A")))) & (Bool (Set (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "e")) ($#k6_domain_1 :::"}"::: ) )) "is" ($#v3_pre_topc :::"independent"::: ) ) ")" ))) ")" )) ; definitioncanceled; let "M" be ($#l1_pre_topc :::"SubsetFamilyStr":::); attr "M" is :::"finite-membered"::: means :: MATROID0:def 6 (Bool (Set ($#k1_matroid0 :::"the_family_of"::: ) "M") "is" ($#v5_finset_1 :::"finite-membered"::: ) ); end; :: deftheorem MATROID0:def 5 : canceled; :: deftheorem defines :::"finite-membered"::: MATROID0:def 6 : (Bool "for" (Set (Var "M")) "being" ($#l1_pre_topc :::"SubsetFamilyStr":::) "holds" (Bool "(" (Bool (Set (Var "M")) "is" ($#v3_matroid0 :::"finite-membered"::: ) ) "iff" (Bool (Set ($#k1_matroid0 :::"the_family_of"::: ) (Set (Var "M"))) "is" ($#v5_finset_1 :::"finite-membered"::: ) ) ")" )); definitionlet "M" be ($#l1_pre_topc :::"SubsetFamilyStr":::); attr "M" is :::"finite-degree"::: means :: MATROID0:def 7 (Bool "(" (Bool "M" "is" ($#v3_matroid0 :::"finite-membered"::: ) ) & (Bool "ex" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "for" (Set (Var "A")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" "M" "st" (Bool (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"independent"::: ) )) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "A"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))))) ")" ); end; :: deftheorem defines :::"finite-degree"::: MATROID0:def 7 : (Bool "for" (Set (Var "M")) "being" ($#l1_pre_topc :::"SubsetFamilyStr":::) "holds" (Bool "(" (Bool (Set (Var "M")) "is" ($#v4_matroid0 :::"finite-degree"::: ) ) "iff" (Bool "(" (Bool (Set (Var "M")) "is" ($#v3_matroid0 :::"finite-membered"::: ) ) & (Bool "ex" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "for" (Set (Var "A")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"independent"::: ) )) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "A"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))))) ")" ) ")" )); registration cluster ($#v4_matroid0 :::"finite-degree"::: ) -> ($#v3_matroid0 :::"finite-membered"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; cluster ($#v8_struct_0 :::"finite"::: ) -> ($#v4_matroid0 :::"finite-degree"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; end; begin registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v4_taxonom2 :::"mutually-disjoint"::: ) ($#v1_setfam_1 :::"with_non-empty_elements"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: MATROID0:5 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "A"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "B"))))) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "B")) ($#k6_subset_1 :::"\"::: ) (Set (Var "A")))))) ; theorem :: MATROID0:6 (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v4_taxonom2 :::"mutually-disjoint"::: ) ($#v1_setfam_1 :::"with_non-empty_elements"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_orders_1 :::"Choice_Function"::: ) "of" (Set (Var "P")) "holds" (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ))) ; registration cluster ($#v1_tdlat_3 :::"discrete"::: ) -> ($#v1_tdlat_3 :::"discrete"::: ) ($#~v3_pencil_1 "non" ($#v3_pencil_1 :::"void"::: ) ) ($#v1_matroid0 :::"subset-closed"::: ) ($#v2_matroid0 :::"with_exchange_property"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; end; theorem :: MATROID0:7 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_tdlat_3 :::"discrete"::: ) ($#l1_pre_topc :::"TopStruct"::: ) "holds" (Bool (Set (Var "T")) "is" ($#l1_pre_topc :::"Matroid":::))) ; definitionlet "P" be ($#m1_hidden :::"set"::: ) ; func :::"ProdMatroid"::: "P" -> ($#v1_pre_topc :::"strict"::: ) ($#l1_pre_topc :::"SubsetFamilyStr":::) means :: MATROID0:def 8 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "P")) & (Bool (Set ($#k1_matroid0 :::"the_family_of"::: ) it) ($#r1_hidden :::"="::: ) "{" (Set (Var "A")) where A "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_tarski :::"union"::: ) "P" ")" ) : (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "D")) ($#r2_hidden :::"in"::: ) "P")) "holds" (Bool "ex" (Set (Var "d")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Set (Set (Var "A")) ($#k8_subset_1 :::"/\"::: ) (Set (Var "D"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "d")) ($#k1_tarski :::"}"::: ) )))) "}" ) ")" ); end; :: deftheorem defines :::"ProdMatroid"::: MATROID0:def 8 : (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#v1_pre_topc :::"strict"::: ) ($#l1_pre_topc :::"SubsetFamilyStr":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k2_matroid0 :::"ProdMatroid"::: ) (Set (Var "P")))) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set (Var "P")))) & (Bool (Set ($#k1_matroid0 :::"the_family_of"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "A")) where A "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_tarski :::"union"::: ) (Set (Var "P")) ")" ) : (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "D")) ($#r2_hidden :::"in"::: ) (Set (Var "P")))) "holds" (Bool "ex" (Set (Var "d")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Set (Set (Var "A")) ($#k8_subset_1 :::"/\"::: ) (Set (Var "D"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "d")) ($#k1_tarski :::"}"::: ) )))) "}" ) ")" ) ")" ))); registrationlet "P" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_setfam_1 :::"with_non-empty_elements"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k2_matroid0 :::"ProdMatroid"::: ) "P") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ; end; theorem :: MATROID0:8 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_matroid0 :::"ProdMatroid"::: ) (Set (Var "P")) ")" ) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"independent"::: ) ) "iff" (Bool "for" (Set (Var "D")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "P")) (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "st" (Bool (Set (Set (Var "A")) ($#k8_subset_1 :::"/\"::: ) (Set (Var "D"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "d")) ($#k1_tarski :::"}"::: ) )))) ")" ))) ; registrationlet "P" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k2_matroid0 :::"ProdMatroid"::: ) "P") -> ($#v1_pre_topc :::"strict"::: ) ($#~v3_pencil_1 "non" ($#v3_pencil_1 :::"void"::: ) ) ($#v1_matroid0 :::"subset-closed"::: ) ; end; theorem :: MATROID0:9 (Bool "for" (Set (Var "P")) "being" ($#v4_taxonom2 :::"mutually-disjoint"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_matroid0 :::"ProdMatroid"::: ) (Set (Var "P")) ")" ) (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "x")) "," (Set (Var "P")) "st" (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "x")))) "holds" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))))))) ; theorem :: MATROID0:10 (Bool "for" (Set (Var "P")) "being" ($#v4_taxonom2 :::"mutually-disjoint"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_matroid0 :::"ProdMatroid"::: ) (Set (Var "P")) ")" ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "x")) "," (Set (Var "P")) "st" (Bool (Bool "(" "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "x")))) "holds" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))) ")" )) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#v3_pre_topc :::"independent"::: ) ) "iff" (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) ")" )))) ; registrationlet "P" be ($#v4_taxonom2 :::"mutually-disjoint"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k2_matroid0 :::"ProdMatroid"::: ) "P") -> ($#v1_pre_topc :::"strict"::: ) ($#v2_matroid0 :::"with_exchange_property"::: ) ; end; registrationlet "X" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; let "P" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set (Const "X")) ")" ); cluster (Set ($#k2_matroid0 :::"ProdMatroid"::: ) "P") -> ($#v8_struct_0 :::"finite"::: ) ($#v1_pre_topc :::"strict"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster -> ($#v4_taxonom2 :::"mutually-disjoint"::: ) for ($#m1_eqrel_1 :::"a_partition"::: ) "of" "X"; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#v1_pre_topc :::"strict"::: ) ($#~v3_pencil_1 "non" ($#v3_pencil_1 :::"void"::: ) ) ($#v1_matroid0 :::"subset-closed"::: ) ($#v2_matroid0 :::"with_exchange_property"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; end; registrationlet "M" be ($#~v3_pencil_1 "non" ($#v3_pencil_1 :::"void"::: ) ) ($#v3_matroid0 :::"finite-membered"::: ) ($#l1_pre_topc :::"SubsetFamilyStr":::); cluster ($#v3_pre_topc :::"independent"::: ) -> ($#v1_finset_1 :::"finite"::: ) ($#v3_pre_topc :::"independent"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M"))); end; definitionlet "F" be ($#l6_algstr_0 :::"Field":::); let "V" be ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "F")); func :::"LinearlyIndependentSubsets"::: "V" -> ($#v1_pre_topc :::"strict"::: ) ($#l1_pre_topc :::"SubsetFamilyStr":::) means :: MATROID0:def 9 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V")) & (Bool (Set ($#k1_matroid0 :::"the_family_of"::: ) it) ($#r1_hidden :::"="::: ) "{" (Set (Var "A")) where A "is" ($#m1_subset_1 :::"Subset":::) "of" "V" : (Bool (Set (Var "A")) "is" ($#v1_vectsp_7 :::"linearly-independent"::: ) ) "}" ) ")" ); end; :: deftheorem defines :::"LinearlyIndependentSubsets"::: MATROID0:def 9 : (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "b3")) "being" ($#v1_pre_topc :::"strict"::: ) ($#l1_pre_topc :::"SubsetFamilyStr":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k3_matroid0 :::"LinearlyIndependentSubsets"::: ) (Set (Var "V")))) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V")))) & (Bool (Set ($#k1_matroid0 :::"the_family_of"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "A")) where A "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) : (Bool (Set (Var "A")) "is" ($#v1_vectsp_7 :::"linearly-independent"::: ) ) "}" ) ")" ) ")" )))); registrationlet "F" be ($#l6_algstr_0 :::"Field":::); let "V" be ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "F")); cluster (Set ($#k3_matroid0 :::"LinearlyIndependentSubsets"::: ) "V") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ($#~v3_pencil_1 "non" ($#v3_pencil_1 :::"void"::: ) ) ($#v1_matroid0 :::"subset-closed"::: ) ; end; theorem :: MATROID0:11 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_matroid0 :::"LinearlyIndependentSubsets"::: ) (Set (Var "V")) ")" ) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"independent"::: ) ) "iff" (Bool (Set (Var "A")) "is" ($#v1_vectsp_7 :::"linearly-independent"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))) ")" )))) ; theorem :: MATROID0:12 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Var "A")))) "holds" (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "v")) ($#r1_struct_0 :::"in"::: ) (Set ($#k1_vectsp_7 :::"Lin"::: ) (Set (Var "A")))) & (Bool (Bool "not" (Set (Var "v")) ($#r1_struct_0 :::"in"::: ) (Set ($#k1_vectsp_7 :::"Lin"::: ) (Set (Var "B")))))) "holds" (Bool "ex" (Set (Var "w")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k7_subset_1 :::"\"::: ) (Set (Var "B")))) & (Bool (Set (Var "w")) ($#r1_struct_0 :::"in"::: ) (Set ($#k1_vectsp_7 :::"Lin"::: ) (Set "(" (Set "(" (Set (Var "A")) ($#k7_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "w")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) ")" ))) ")" )))))) ; theorem :: MATROID0:13 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v1_vectsp_7 :::"linearly-independent"::: ) )) "holds" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"nin"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_vectsp_7 :::"Lin"::: ) (Set (Var "A")) ")" )))) "holds" (Bool (Set (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "a")) ($#k6_domain_1 :::"}"::: ) )) "is" ($#v1_vectsp_7 :::"linearly-independent"::: ) ))))) ; registrationlet "F" be ($#l6_algstr_0 :::"Field":::); let "V" be ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "F")); cluster (Set ($#k3_matroid0 :::"LinearlyIndependentSubsets"::: ) "V") -> ($#v1_pre_topc :::"strict"::: ) ($#v2_matroid0 :::"with_exchange_property"::: ) ; end; registrationlet "F" be ($#l6_algstr_0 :::"Field":::); let "V" be ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "F")); cluster (Set ($#k3_matroid0 :::"LinearlyIndependentSubsets"::: ) "V") -> ($#v1_pre_topc :::"strict"::: ) ($#v3_matroid0 :::"finite-membered"::: ) ; end; begin definitionlet "M" be ($#l1_pre_topc :::"SubsetFamilyStr":::); let "A", "C" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "M")); pred "A" :::"is_maximal_independent_in"::: "C" means :: MATROID0:def 10 (Bool "(" (Bool "A" "is" ($#v3_pre_topc :::"independent"::: ) ) & (Bool "A" ($#r1_tarski :::"c="::: ) "C") & (Bool "(" "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" "M" "st" (Bool (Bool (Set (Var "B")) "is" ($#v3_pre_topc :::"independent"::: ) ) & (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) "C") & (Bool "A" ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool "A" ($#r1_hidden :::"="::: ) (Set (Var "B"))) ")" ) ")" ); end; :: deftheorem defines :::"is_maximal_independent_in"::: MATROID0:def 10 : (Bool "for" (Set (Var "M")) "being" ($#l1_pre_topc :::"SubsetFamilyStr":::) (Bool "for" (Set (Var "A")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r1_matroid0 :::"is_maximal_independent_in"::: ) (Set (Var "C"))) "iff" (Bool "(" (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"independent"::: ) ) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "C"))) & (Bool "(" "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "B")) "is" ($#v3_pre_topc :::"independent"::: ) ) & (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "B"))) ")" ) ")" ) ")" ))); theorem :: MATROID0:14 (Bool "for" (Set (Var "M")) "being" ($#~v3_pencil_1 "non" ($#v3_pencil_1 :::"void"::: ) ) ($#v4_matroid0 :::"finite-degree"::: ) ($#l1_pre_topc :::"SubsetFamilyStr":::) (Bool "for" (Set (Var "C")) "," (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"independent"::: ) )) "holds" (Bool "ex" (Set (Var "B")) "being" ($#v3_pre_topc :::"independent"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) "st" (Bool "(" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B"))) & (Bool (Set (Var "B")) ($#r1_matroid0 :::"is_maximal_independent_in"::: ) (Set (Var "C"))) ")" )))) ; theorem :: MATROID0:15 (Bool "for" (Set (Var "M")) "being" ($#~v3_pencil_1 "non" ($#v3_pencil_1 :::"void"::: ) ) ($#v1_matroid0 :::"subset-closed"::: ) ($#v4_matroid0 :::"finite-degree"::: ) ($#l1_pre_topc :::"SubsetFamilyStr":::) (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) (Bool "ex" (Set (Var "A")) "being" ($#v3_pre_topc :::"independent"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) "st" (Bool (Set (Var "A")) ($#r1_matroid0 :::"is_maximal_independent_in"::: ) (Set (Var "C")))))) ; theorem :: MATROID0:16 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v3_pencil_1 "non" ($#v3_pencil_1 :::"void"::: ) ) ($#v1_matroid0 :::"subset-closed"::: ) ($#v4_matroid0 :::"finite-degree"::: ) ($#l1_pre_topc :::"SubsetFamilyStr":::) "holds" (Bool "(" (Bool (Set (Var "M")) "is" ($#l1_pre_topc :::"Matroid":::)) "iff" (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v3_pre_topc :::"independent"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "A")) ($#r1_matroid0 :::"is_maximal_independent_in"::: ) (Set (Var "C"))) & (Bool (Set (Var "B")) ($#r1_matroid0 :::"is_maximal_independent_in"::: ) (Set (Var "C")))) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "B")))))) ")" )) ; definitionlet "M" be ($#v4_matroid0 :::"finite-degree"::: ) ($#l1_pre_topc :::"Matroid":::); let "C" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "M")); func :::"Rnk"::: "C" -> ($#m1_hidden :::"Nat":::) equals :: MATROID0:def 11 (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "A")) ")" ) where A "is" ($#v3_pre_topc :::"independent"::: ) ($#m1_subset_1 :::"Subset":::) "of" "M" : (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) "C") "}" ); end; :: deftheorem defines :::"Rnk"::: MATROID0:def 11 : (Bool "for" (Set (Var "M")) "being" ($#v4_matroid0 :::"finite-degree"::: ) ($#l1_pre_topc :::"Matroid":::) (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) "holds" (Bool (Set ($#k4_matroid0 :::"Rnk"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "A")) ")" ) where A "is" ($#v3_pre_topc :::"independent"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) : (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "C"))) "}" )))); theorem :: MATROID0:17 (Bool "for" (Set (Var "M")) "being" ($#v4_matroid0 :::"finite-degree"::: ) ($#l1_pre_topc :::"Matroid":::) (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "A")) "being" ($#v3_pre_topc :::"independent"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "C")))) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "A"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k4_matroid0 :::"Rnk"::: ) (Set (Var "C"))))))) ; theorem :: MATROID0:18 (Bool "for" (Set (Var "M")) "being" ($#v4_matroid0 :::"finite-degree"::: ) ($#l1_pre_topc :::"Matroid":::) (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) (Bool "ex" (Set (Var "A")) "being" ($#v3_pre_topc :::"independent"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) "st" (Bool "(" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "C"))) & (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k4_matroid0 :::"Rnk"::: ) (Set (Var "C")))) ")" )))) ; theorem :: MATROID0:19 (Bool "for" (Set (Var "M")) "being" ($#v4_matroid0 :::"finite-degree"::: ) ($#l1_pre_topc :::"Matroid":::) (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "A")) "being" ($#v3_pre_topc :::"independent"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r1_matroid0 :::"is_maximal_independent_in"::: ) (Set (Var "C"))) "iff" (Bool "(" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "C"))) & (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k4_matroid0 :::"Rnk"::: ) (Set (Var "C")))) ")" ) ")" )))) ; theorem :: MATROID0:20 (Bool "for" (Set (Var "M")) "being" ($#v4_matroid0 :::"finite-degree"::: ) ($#l1_pre_topc :::"Matroid":::) (Bool "for" (Set (Var "C")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) "holds" (Bool (Set ($#k4_matroid0 :::"Rnk"::: ) (Set (Var "C"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "C")))))) ; theorem :: MATROID0:21 (Bool "for" (Set (Var "M")) "being" ($#v4_matroid0 :::"finite-degree"::: ) ($#l1_pre_topc :::"Matroid":::) (Bool "for" (Set (Var "C")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "C")) "is" ($#v3_pre_topc :::"independent"::: ) ) "iff" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k4_matroid0 :::"Rnk"::: ) (Set (Var "C")))) ")" ))) ; definitionlet "M" be ($#v4_matroid0 :::"finite-degree"::: ) ($#l1_pre_topc :::"Matroid":::); func :::"Rnk"::: "M" -> ($#m1_hidden :::"Nat":::) equals :: MATROID0:def 12 (Set ($#k4_matroid0 :::"Rnk"::: ) (Set "(" ($#k2_struct_0 :::"[#]"::: ) "M" ")" )); end; :: deftheorem defines :::"Rnk"::: MATROID0:def 12 : (Bool "for" (Set (Var "M")) "being" ($#v4_matroid0 :::"finite-degree"::: ) ($#l1_pre_topc :::"Matroid":::) "holds" (Bool (Set ($#k5_matroid0 :::"Rnk"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k4_matroid0 :::"Rnk"::: ) (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "M")) ")" )))); definitionlet "M" be ($#~v3_pencil_1 "non" ($#v3_pencil_1 :::"void"::: ) ) ($#v4_matroid0 :::"finite-degree"::: ) ($#l1_pre_topc :::"SubsetFamilyStr":::); mode :::"Basis"::: "of" "M" -> ($#v3_pre_topc :::"independent"::: ) ($#m1_subset_1 :::"Subset":::) "of" "M" means :: MATROID0:def 13 (Bool it ($#r1_matroid0 :::"is_maximal_independent_in"::: ) (Set ($#k2_struct_0 :::"[#]"::: ) "M")); end; :: deftheorem defines :::"Basis"::: MATROID0:def 13 : (Bool "for" (Set (Var "M")) "being" ($#~v3_pencil_1 "non" ($#v3_pencil_1 :::"void"::: ) ) ($#v4_matroid0 :::"finite-degree"::: ) ($#l1_pre_topc :::"SubsetFamilyStr":::) (Bool "for" (Set (Var "b2")) "being" ($#v3_pre_topc :::"independent"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_matroid0 :::"Basis"::: ) "of" (Set (Var "M"))) "iff" (Bool (Set (Var "b2")) ($#r1_matroid0 :::"is_maximal_independent_in"::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "M")))) ")" ))); theorem :: MATROID0:22 (Bool "for" (Set (Var "M")) "being" ($#v4_matroid0 :::"finite-degree"::: ) ($#l1_pre_topc :::"Matroid":::) (Bool "for" (Set (Var "B1")) "," (Set (Var "B2")) "being" ($#m1_matroid0 :::"Basis"::: ) "of" (Set (Var "M")) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "B1"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "B2")))))) ; theorem :: MATROID0:23 (Bool "for" (Set (Var "M")) "being" ($#v4_matroid0 :::"finite-degree"::: ) ($#l1_pre_topc :::"Matroid":::) (Bool "for" (Set (Var "A")) "being" ($#v3_pre_topc :::"independent"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) (Bool "ex" (Set (Var "B")) "being" ($#m1_matroid0 :::"Basis"::: ) "of" (Set (Var "M")) "st" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))))) ; theorem :: MATROID0:24 (Bool "for" (Set (Var "M")) "being" ($#v4_matroid0 :::"finite-degree"::: ) ($#l1_pre_topc :::"Matroid":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set ($#k4_matroid0 :::"Rnk"::: ) (Set (Var "A"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k4_matroid0 :::"Rnk"::: ) (Set (Var "B")))))) ; theorem :: MATROID0:25 (Bool "for" (Set (Var "M")) "being" ($#v4_matroid0 :::"finite-degree"::: ) ($#l1_pre_topc :::"Matroid":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) "holds" (Bool (Set (Set "(" ($#k4_matroid0 :::"Rnk"::: ) (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k4_matroid0 :::"Rnk"::: ) (Set "(" (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B")) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k4_matroid0 :::"Rnk"::: ) (Set (Var "A")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k4_matroid0 :::"Rnk"::: ) (Set (Var "B")) ")" ))))) ; theorem :: MATROID0:26 (Bool "for" (Set (Var "M")) "being" ($#v4_matroid0 :::"finite-degree"::: ) ($#l1_pre_topc :::"Matroid":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set ($#k4_matroid0 :::"Rnk"::: ) (Set (Var "A"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k4_matroid0 :::"Rnk"::: ) (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B")) ")" ))) & (Bool (Set ($#k4_matroid0 :::"Rnk"::: ) (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "e")) ($#k6_domain_1 :::"}"::: ) ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k4_matroid0 :::"Rnk"::: ) (Set (Var "A")) ")" ) ($#k1_nat_1 :::"+"::: ) (Num 1))) ")" )))) ; theorem :: MATROID0:27 (Bool "for" (Set (Var "M")) "being" ($#v4_matroid0 :::"finite-degree"::: ) ($#l1_pre_topc :::"Matroid":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "e")) "," (Set (Var "f")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set ($#k4_matroid0 :::"Rnk"::: ) (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "e")) ($#k6_domain_1 :::"}"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_matroid0 :::"Rnk"::: ) (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "f")) ($#k6_domain_1 :::"}"::: ) ) ")" ))) & (Bool (Set ($#k4_matroid0 :::"Rnk"::: ) (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "f")) ($#k6_domain_1 :::"}"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_matroid0 :::"Rnk"::: ) (Set (Var "A"))))) "holds" (Bool (Set ($#k4_matroid0 :::"Rnk"::: ) (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "e")) "," (Set (Var "f")) ($#k7_domain_1 :::"}"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_matroid0 :::"Rnk"::: ) (Set (Var "A"))))))) ; begin definitionlet "M" be ($#v4_matroid0 :::"finite-degree"::: ) ($#l1_pre_topc :::"Matroid":::); let "e" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "M")); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "M")); pred "e" :::"is_dependent_on"::: "A" means :: MATROID0:def 14 (Bool (Set ($#k4_matroid0 :::"Rnk"::: ) (Set "(" "A" ($#k4_subset_1 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) "e" ($#k6_domain_1 :::"}"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_matroid0 :::"Rnk"::: ) "A")); end; :: deftheorem defines :::"is_dependent_on"::: MATROID0:def 14 : (Bool "for" (Set (Var "M")) "being" ($#v4_matroid0 :::"finite-degree"::: ) ($#l1_pre_topc :::"Matroid":::) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "e")) ($#r2_matroid0 :::"is_dependent_on"::: ) (Set (Var "A"))) "iff" (Bool (Set ($#k4_matroid0 :::"Rnk"::: ) (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "e")) ($#k6_domain_1 :::"}"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_matroid0 :::"Rnk"::: ) (Set (Var "A")))) ")" )))); theorem :: MATROID0:28 (Bool "for" (Set (Var "M")) "being" ($#v4_matroid0 :::"finite-degree"::: ) ($#l1_pre_topc :::"Matroid":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "e")) ($#r2_matroid0 :::"is_dependent_on"::: ) (Set (Var "A")))))) ; theorem :: MATROID0:29 (Bool "for" (Set (Var "M")) "being" ($#v4_matroid0 :::"finite-degree"::: ) ($#l1_pre_topc :::"Matroid":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B"))) & (Bool (Set (Var "e")) ($#r2_matroid0 :::"is_dependent_on"::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "e")) ($#r2_matroid0 :::"is_dependent_on"::: ) (Set (Var "B")))))) ; definitionlet "M" be ($#v4_matroid0 :::"finite-degree"::: ) ($#l1_pre_topc :::"Matroid":::); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "M")); func :::"Span"::: "A" -> ($#m1_subset_1 :::"Subset":::) "of" "M" equals :: MATROID0:def 15 "{" (Set (Var "e")) where e "is" ($#m1_subset_1 :::"Element":::) "of" "M" : (Bool (Set (Var "e")) ($#r2_matroid0 :::"is_dependent_on"::: ) "A") "}" ; end; :: deftheorem defines :::"Span"::: MATROID0:def 15 : (Bool "for" (Set (Var "M")) "being" ($#v4_matroid0 :::"finite-degree"::: ) ($#l1_pre_topc :::"Matroid":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) "holds" (Bool (Set ($#k6_matroid0 :::"Span"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "e")) where e "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) : (Bool (Set (Var "e")) ($#r2_matroid0 :::"is_dependent_on"::: ) (Set (Var "A"))) "}" ))); theorem :: MATROID0:30 (Bool "for" (Set (Var "M")) "being" ($#v4_matroid0 :::"finite-degree"::: ) ($#l1_pre_topc :::"Matroid":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set ($#k6_matroid0 :::"Span"::: ) (Set (Var "A")))) "iff" (Bool (Set ($#k4_matroid0 :::"Rnk"::: ) (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "e")) ($#k6_domain_1 :::"}"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_matroid0 :::"Rnk"::: ) (Set (Var "A")))) ")" )))) ; theorem :: MATROID0:31 (Bool "for" (Set (Var "M")) "being" ($#v4_matroid0 :::"finite-degree"::: ) ($#l1_pre_topc :::"Matroid":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) "holds" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k6_matroid0 :::"Span"::: ) (Set (Var "A")))))) ; theorem :: MATROID0:32 (Bool "for" (Set (Var "M")) "being" ($#v4_matroid0 :::"finite-degree"::: ) ($#l1_pre_topc :::"Matroid":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set ($#k6_matroid0 :::"Span"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set ($#k6_matroid0 :::"Span"::: ) (Set (Var "B")))))) ; theorem :: MATROID0:33 (Bool "for" (Set (Var "M")) "being" ($#v4_matroid0 :::"finite-degree"::: ) ($#l1_pre_topc :::"Matroid":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) "holds" (Bool (Set ($#k4_matroid0 :::"Rnk"::: ) (Set "(" ($#k6_matroid0 :::"Span"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_matroid0 :::"Rnk"::: ) (Set (Var "A")))))) ; theorem :: MATROID0:34 (Bool "for" (Set (Var "M")) "being" ($#v4_matroid0 :::"finite-degree"::: ) ($#l1_pre_topc :::"Matroid":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "e")) ($#r2_matroid0 :::"is_dependent_on"::: ) (Set ($#k6_matroid0 :::"Span"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Var "e")) ($#r2_matroid0 :::"is_dependent_on"::: ) (Set (Var "A")))))) ; theorem :: MATROID0:35 (Bool "for" (Set (Var "M")) "being" ($#v4_matroid0 :::"finite-degree"::: ) ($#l1_pre_topc :::"Matroid":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) "holds" (Bool (Set ($#k6_matroid0 :::"Span"::: ) (Set "(" ($#k6_matroid0 :::"Span"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_matroid0 :::"Span"::: ) (Set (Var "A")))))) ; theorem :: MATROID0:36 (Bool "for" (Set (Var "M")) "being" ($#v4_matroid0 :::"finite-degree"::: ) ($#l1_pre_topc :::"Matroid":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "f")) "," (Set (Var "e")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"nin"::: ) (Set ($#k6_matroid0 :::"Span"::: ) (Set (Var "A")))) & (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k6_matroid0 :::"Span"::: ) (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "e")) ($#k6_domain_1 :::"}"::: ) ) ")" )))) "holds" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set ($#k6_matroid0 :::"Span"::: ) (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "f")) ($#k6_domain_1 :::"}"::: ) ) ")" )))))) ; definitionlet "M" be ($#l1_pre_topc :::"SubsetFamilyStr":::); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "M")); attr "A" is :::"cycle"::: means :: MATROID0:def 16 (Bool "(" (Bool "A" "is" ($#v3_pre_topc :::"dependent"::: ) ) & (Bool "(" "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element":::) "of" "M" "st" (Bool (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) "A")) "holds" (Bool (Set "A" ($#k7_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "e")) ($#k1_tarski :::"}"::: ) )) "is" ($#v3_pre_topc :::"independent"::: ) ) ")" ) ")" ); end; :: deftheorem defines :::"cycle"::: MATROID0:def 16 : (Bool "for" (Set (Var "M")) "being" ($#l1_pre_topc :::"SubsetFamilyStr":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v5_matroid0 :::"cycle"::: ) ) "iff" (Bool "(" (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"dependent"::: ) ) & (Bool "(" "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "A")) ($#k7_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "e")) ($#k1_tarski :::"}"::: ) )) "is" ($#v3_pre_topc :::"independent"::: ) ) ")" ) ")" ) ")" ))); theorem :: MATROID0:37 (Bool "for" (Set (Var "M")) "being" ($#v4_matroid0 :::"finite-degree"::: ) ($#l1_pre_topc :::"Matroid":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v5_matroid0 :::"cycle"::: ) )) "holds" (Bool "(" (Bool (Bool "not" (Set (Var "A")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set (Var "A")) "is" ($#v1_finset_1 :::"finite"::: ) ) ")" ))) ; registrationlet "M" be ($#v4_matroid0 :::"finite-degree"::: ) ($#l1_pre_topc :::"Matroid":::); cluster ($#v5_matroid0 :::"cycle"::: ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M"))); end; theorem :: MATROID0:38 (Bool "for" (Set (Var "M")) "being" ($#v4_matroid0 :::"finite-degree"::: ) ($#l1_pre_topc :::"Matroid":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v5_matroid0 :::"cycle"::: ) ) "iff" (Bool "(" (Bool (Bool "not" (Set (Var "A")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool "(" "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "A")) ($#k7_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "e")) ($#k6_domain_1 :::"}"::: ) )) ($#r1_matroid0 :::"is_maximal_independent_in"::: ) (Set (Var "A"))) ")" ) ")" ) ")" ))) ; theorem :: MATROID0:39 (Bool "for" (Set (Var "M")) "being" ($#v4_matroid0 :::"finite-degree"::: ) ($#l1_pre_topc :::"Matroid":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v5_matroid0 :::"cycle"::: ) )) "holds" (Bool (Set (Set "(" ($#k4_matroid0 :::"Rnk"::: ) (Set (Var "A")) ")" ) ($#k1_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set (Var "A")))))) ; theorem :: MATROID0:40 (Bool "for" (Set (Var "M")) "being" ($#v4_matroid0 :::"finite-degree"::: ) ($#l1_pre_topc :::"Matroid":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v5_matroid0 :::"cycle"::: ) ) & (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "e")) ($#r2_matroid0 :::"is_dependent_on"::: ) (Set (Set (Var "A")) ($#k7_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "e")) ($#k6_domain_1 :::"}"::: ) )))))) ; theorem :: MATROID0:41 (Bool "for" (Set (Var "M")) "being" ($#v4_matroid0 :::"finite-degree"::: ) ($#l1_pre_topc :::"Matroid":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v5_matroid0 :::"cycle"::: ) ) & (Bool (Set (Var "B")) "is" ($#v5_matroid0 :::"cycle"::: ) ) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "B"))))) ; theorem :: MATROID0:42 (Bool "for" (Set (Var "M")) "being" ($#v4_matroid0 :::"finite-degree"::: ) ($#l1_pre_topc :::"Matroid":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) "st" (Bool (Bool "(" "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Var "A")))) "holds" (Bool "not" (Bool (Set (Var "B")) "is" ($#v5_matroid0 :::"cycle"::: ) )) ")" )) "holds" (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"independent"::: ) ))) ; theorem :: MATROID0:43 (Bool "for" (Set (Var "M")) "being" ($#v4_matroid0 :::"finite-degree"::: ) ($#l1_pre_topc :::"Matroid":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v5_matroid0 :::"cycle"::: ) ) & (Bool (Set (Var "B")) "is" ($#v5_matroid0 :::"cycle"::: ) ) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "B"))) & (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B"))))) "holds" (Bool "ex" (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) "st" (Bool "(" (Bool (Set (Var "C")) "is" ($#v5_matroid0 :::"cycle"::: ) ) & (Bool (Set (Var "C")) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "e")) ($#k6_domain_1 :::"}"::: ) ))) ")" ))))) ; theorem :: MATROID0:44 (Bool "for" (Set (Var "M")) "being" ($#v4_matroid0 :::"finite-degree"::: ) ($#l1_pre_topc :::"Matroid":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"independent"::: ) ) & (Bool (Set (Var "B")) "is" ($#v5_matroid0 :::"cycle"::: ) ) & (Bool (Set (Var "C")) "is" ($#v5_matroid0 :::"cycle"::: ) ) & (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "e")) ($#k6_domain_1 :::"}"::: ) ))) & (Bool (Set (Var "C")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "e")) ($#k6_domain_1 :::"}"::: ) )))) "holds" (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Var "C")))))) ;