:: PENCIL_3 semantic presentation begin theorem :: PENCIL_3:1 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v3_pencil_1 "non" ($#v3_pencil_1 :::"void"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Collineation":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r1_pencil_1 :::"are_collinear"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) "," (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "q"))) ($#r1_pencil_1 :::"are_collinear"::: ) )))) ; theorem :: PENCIL_3:2 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) (Bool "for" (Set (Var "A")) "being" ($#v2_pralg_1 :::"1-sorted-yielding"::: ) ($#v14_pencil_1 :::"non-Trivial-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Bool "not" (Set (Set (Var "A")) ($#k10_pralg_1 :::"."::: ) (Set (Var "i"))) "is" ($#v7_struct_0 :::"trivial"::: ) ))))) ; theorem :: PENCIL_3:3 (Bool "for" (Set (Var "S")) "being" ($#~v3_pencil_1 "non" ($#v3_pencil_1 :::"void"::: ) ) ($#v6_pencil_1 :::"identifying_close_blocks"::: ) ($#l1_pre_topc :::"TopStruct"::: ) "st" (Bool (Bool (Set (Var "S")) "is" ($#v10_pencil_1 :::"strongly_connected"::: ) )) "holds" (Bool (Set (Var "S")) "is" ($#v8_pencil_1 :::"without_isolated_points"::: ) )) ; theorem :: PENCIL_3:4 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v3_pencil_1 "non" ($#v3_pencil_1 :::"void"::: ) ) ($#v6_pencil_1 :::"identifying_close_blocks"::: ) ($#l1_pre_topc :::"TopStruct"::: ) "st" (Bool (Bool (Set (Var "S")) "is" ($#v10_pencil_1 :::"strongly_connected"::: ) )) "holds" (Bool (Set (Var "S")) "is" ($#v9_pencil_1 :::"connected"::: ) )) ; theorem :: PENCIL_3:5 (Bool "for" (Set (Var "S")) "being" ($#~v3_pencil_1 "non" ($#v3_pencil_1 :::"void"::: ) ) ($#~v4_pencil_1 "non" ($#v4_pencil_1 :::"degenerated"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"Block":::) "of" (Set (Var "S")) "holds" (Bool "not" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "L"))))))) ; theorem :: PENCIL_3:6 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_waybel_3 :::"non-Empty"::: ) ($#v11_pencil_1 :::"TopStruct-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k5_pencil_1 :::"Segre_Product"::: ) (Set (Var "A")) ")" ) "holds" (Bool (Set (Var "p")) "is" ($#m1_pboole :::"Element"::: ) "of" (Set ($#k12_pralg_1 :::"Carrier"::: ) (Set (Var "A"))))))) ; theorem :: PENCIL_3:7 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#v2_pralg_1 :::"1-sorted-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) "holds" (Bool (Set (Set "(" ($#k12_pralg_1 :::"Carrier"::: ) (Set (Var "A")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set "(" (Set (Var "A")) ($#k10_pralg_1 :::"."::: ) (Set (Var "x")) ")" )))))) ; theorem :: PENCIL_3:8 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) (Bool "for" (Set (Var "A")) "being" ($#v11_pencil_1 :::"TopStruct-yielding"::: ) ($#v14_pencil_1 :::"non-Trivial-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "ex" (Set (Var "L")) "being" ($#~v13_pencil_1 "non" ($#v13_pencil_1 :::"trivial-yielding"::: ) ) ($#v16_pencil_1 :::"Segre-like"::: ) ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set ($#k12_pralg_1 :::"Carrier"::: ) (Set (Var "A"))) "st" (Bool "(" (Bool (Set ($#k3_pencil_1 :::"indx"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set (Var "i"))) & (Bool (Set ($#k4_card_3 :::"product"::: ) (Set (Var "L"))) "is" ($#m1_pencil_2 :::"Segre-Coset"::: ) "of" (Set (Var "A"))) ")" ))))) ; theorem :: PENCIL_3:9 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) (Bool "for" (Set (Var "A")) "being" ($#v11_pencil_1 :::"TopStruct-yielding"::: ) ($#v14_pencil_1 :::"non-Trivial-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k5_pencil_1 :::"Segre_Product"::: ) (Set (Var "A")) ")" ) (Bool "ex" (Set (Var "L")) "being" ($#~v13_pencil_1 "non" ($#v13_pencil_1 :::"trivial-yielding"::: ) ) ($#v16_pencil_1 :::"Segre-like"::: ) ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set ($#k12_pralg_1 :::"Carrier"::: ) (Set (Var "A"))) "st" (Bool "(" (Bool (Set ($#k3_pencil_1 :::"indx"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set (Var "i"))) & (Bool (Set ($#k4_card_3 :::"product"::: ) (Set (Var "L"))) "is" ($#m1_pencil_2 :::"Segre-Coset"::: ) "of" (Set (Var "A"))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k4_card_3 :::"product"::: ) (Set (Var "L")))) ")" )))))) ; theorem :: PENCIL_3:10 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#v11_pencil_1 :::"TopStruct-yielding"::: ) ($#v14_pencil_1 :::"non-Trivial-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "b")) "being" ($#~v13_pencil_1 "non" ($#v13_pencil_1 :::"trivial-yielding"::: ) ) ($#v16_pencil_1 :::"Segre-like"::: ) ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set ($#k12_pralg_1 :::"Carrier"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set ($#k4_card_3 :::"product"::: ) (Set (Var "b"))) "is" ($#m1_pencil_2 :::"Segre-Coset"::: ) "of" (Set (Var "A")))) "holds" (Bool (Set (Set (Var "b")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_pencil_1 :::"indx"::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set "(" (Set (Var "A")) ($#k1_pencil_1 :::"."::: ) (Set "(" ($#k3_pencil_1 :::"indx"::: ) (Set (Var "b")) ")" ) ")" )))))) ; theorem :: PENCIL_3:11 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#v11_pencil_1 :::"TopStruct-yielding"::: ) ($#v14_pencil_1 :::"non-Trivial-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#~v13_pencil_1 "non" ($#v13_pencil_1 :::"trivial-yielding"::: ) ) ($#v16_pencil_1 :::"Segre-like"::: ) ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set ($#k12_pralg_1 :::"Carrier"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set ($#k4_card_3 :::"product"::: ) (Set (Var "L1"))) "is" ($#m1_pencil_2 :::"Segre-Coset"::: ) "of" (Set (Var "A"))) & (Bool (Set ($#k4_card_3 :::"product"::: ) (Set (Var "L2"))) "is" ($#m1_pencil_2 :::"Segre-Coset"::: ) "of" (Set (Var "A"))) & (Bool (Set ($#k3_pencil_1 :::"indx"::: ) (Set (Var "L1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_pencil_1 :::"indx"::: ) (Set (Var "L2")))) & (Bool (Set ($#k4_card_3 :::"product"::: ) (Set (Var "L1"))) ($#r2_subset_1 :::"meets"::: ) (Set ($#k4_card_3 :::"product"::: ) (Set (Var "L2"))))) "holds" (Bool (Set (Var "L1")) ($#r8_pboole :::"="::: ) (Set (Var "L2")))))) ; theorem :: PENCIL_3:12 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#v15_pencil_1 :::"PLS-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "L")) "being" ($#~v13_pencil_1 "non" ($#v13_pencil_1 :::"trivial-yielding"::: ) ) ($#v16_pencil_1 :::"Segre-like"::: ) ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set ($#k12_pralg_1 :::"Carrier"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Block":::) "of" (Set "(" (Set (Var "A")) ($#k2_pencil_1 :::"."::: ) (Set "(" ($#k3_pencil_1 :::"indx"::: ) (Set (Var "L")) ")" ) ")" ) "holds" (Bool (Set ($#k4_card_3 :::"product"::: ) (Set "(" (Set (Var "L")) ($#k2_funct_7 :::"+*"::: ) "(" (Set "(" ($#k3_pencil_1 :::"indx"::: ) (Set (Var "L")) ")" ) "," (Set (Var "B")) ")" ")" )) "is" ($#m1_subset_1 :::"Block":::) "of" (Set "(" ($#k5_pencil_1 :::"Segre_Product"::: ) (Set (Var "A")) ")" )))))) ; theorem :: PENCIL_3:13 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#v15_pencil_1 :::"PLS-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" (Set (Var "A")) ($#k2_pencil_1 :::"."::: ) (Set (Var "i")) ")" ) (Bool "for" (Set (Var "L")) "being" ($#~v13_pencil_1 "non" ($#v13_pencil_1 :::"trivial-yielding"::: ) ) ($#v16_pencil_1 :::"Segre-like"::: ) ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set ($#k12_pralg_1 :::"Carrier"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set ($#k3_pencil_1 :::"indx"::: ) (Set (Var "L"))))) "holds" (Bool (Set (Set (Var "L")) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "p")) ($#k6_domain_1 :::"}"::: ) ) ")" ) "is" ($#~v13_pencil_1 "non" ($#v13_pencil_1 :::"trivial-yielding"::: ) ) ($#v16_pencil_1 :::"Segre-like"::: ) ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set ($#k12_pralg_1 :::"Carrier"::: ) (Set (Var "A"))))))))) ; theorem :: PENCIL_3:14 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#v15_pencil_1 :::"PLS-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "A")) ($#k2_pencil_1 :::"."::: ) (Set (Var "i")) ")" ) (Bool "for" (Set (Var "L")) "being" ($#~v13_pencil_1 "non" ($#v13_pencil_1 :::"trivial-yielding"::: ) ) ($#v16_pencil_1 :::"Segre-like"::: ) ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set ($#k12_pralg_1 :::"Carrier"::: ) (Set (Var "A"))) "holds" (Bool (Set ($#k4_card_3 :::"product"::: ) (Set "(" (Set (Var "L")) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set (Var "S")) ")" ")" )) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k5_pencil_1 :::"Segre_Product"::: ) (Set (Var "A")) ")" ))))))) ; theorem :: PENCIL_3:15 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) "holds" (Bool (Set (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "P")) ($#k1_pzfmisc1 :::"}"::: ) ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) "is" (Num 1) ($#v3_card_1 :::"-element"::: ) )))) ; theorem :: PENCIL_3:16 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) (Bool "for" (Set (Var "A")) "being" ($#v15_pencil_1 :::"PLS-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Block":::) "of" (Set "(" (Set (Var "A")) ($#k2_pencil_1 :::"."::: ) (Set (Var "i")) ")" ) (Bool "for" (Set (Var "P")) "being" ($#m1_pboole :::"Element"::: ) "of" (Set ($#k12_pralg_1 :::"Carrier"::: ) (Set (Var "A"))) "holds" (Bool (Set ($#k4_card_3 :::"product"::: ) (Set "(" (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "P")) ($#k1_pzfmisc1 :::"}"::: ) ) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set (Var "B")) ")" ")" )) "is" ($#m1_subset_1 :::"Block":::) "of" (Set "(" ($#k5_pencil_1 :::"Segre_Product"::: ) (Set (Var "A")) ")" ))))))) ; theorem :: PENCIL_3:17 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#v15_pencil_1 :::"PLS-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k5_pencil_1 :::"Segre_Product"::: ) (Set (Var "A")) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "q")))) "holds" (Bool "(" (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r1_pencil_1 :::"are_collinear"::: ) ) "iff" (Bool "for" (Set (Var "p1")) "," (Set (Var "q1")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "p1")) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set (Var "q1")) ($#r1_hidden :::"="::: ) (Set (Var "q")))) "holds" (Bool "ex" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) "st" (Bool "(" (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" (Set (Var "A")) ($#k2_pencil_1 :::"."::: ) (Set (Var "i")) ")" ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p1")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Set (Var "q1")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_pencil_1 :::"are_collinear"::: ) ) ")" ) ")" ) & (Bool "(" "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "j")) ($#r1_hidden :::"<>"::: ) (Set (Var "i")))) "holds" (Bool (Set (Set (Var "p1")) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "q1")) ($#k1_funct_1 :::"."::: ) (Set (Var "j")))) ")" ) ")" ))) ")" )))) ; theorem :: PENCIL_3:18 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#v15_pencil_1 :::"PLS-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "b")) "being" ($#~v13_pencil_1 "non" ($#v13_pencil_1 :::"trivial-yielding"::: ) ) ($#v16_pencil_1 :::"Segre-like"::: ) ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set ($#k12_pralg_1 :::"Carrier"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" (Set (Var "A")) ($#k2_pencil_1 :::"."::: ) (Set "(" ($#k3_pencil_1 :::"indx"::: ) (Set (Var "b")) ")" ) ")" ) (Bool "ex" (Set (Var "p")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k4_card_3 :::"product"::: ) (Set (Var "b")))) & (Bool (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "p")) ($#k2_funct_7 :::"+*"::: ) "(" (Set "(" ($#k3_pencil_1 :::"indx"::: ) (Set (Var "b")) ")" ) "," (Set (Var "x")) ")" ")" ) ($#k1_tarski :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_card_3 :::"product"::: ) (Set "(" (Set (Var "b")) ($#k2_funct_7 :::"+*"::: ) "(" (Set "(" ($#k3_pencil_1 :::"indx"::: ) (Set (Var "b")) ")" ) "," (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) ")" ")" ))) ")" )))))) ; definitionlet "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; let "b1", "b2" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); func :::"diff"::: "(" "b1" "," "b2" ")" -> ($#m1_hidden :::"Nat":::) equals :: PENCIL_3:def 1 (Set ($#k1_card_1 :::"card"::: ) "{" (Set (Var "i")) where i "is" ($#m1_subset_1 :::"Element"::: ) "of" "I" : (Bool (Set "b1" ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"<>"::: ) (Set "b2" ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) "}" ); end; :: deftheorem defines :::"diff"::: PENCIL_3:def 1 : (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set ($#k1_pencil_3 :::"diff"::: ) "(" (Set (Var "b1")) "," (Set (Var "b2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) "{" (Set (Var "i")) where i "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) : (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) "}" )))); theorem :: PENCIL_3:19 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool (Set ($#k1_pencil_3 :::"diff"::: ) "(" (Set (Var "b1")) "," (Set (Var "b2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_pencil_3 :::"diff"::: ) "(" (Set (Var "b1")) "," (Set "(" (Set (Var "b2")) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set "(" (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ")" ")" ) ")" ")" ) ($#k1_nat_1 :::"+"::: ) (Num 1)))))) ; begin definitionlet "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "A" be ($#v15_pencil_1 :::"PLS-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); let "B1", "B2" be ($#m1_pencil_2 :::"Segre-Coset"::: ) "of" (Set (Const "A")); pred "B1" :::"'||'"::: "B2" means :: PENCIL_3:def 2 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k5_pencil_1 :::"Segre_Product"::: ) "A" ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "B1")) "holds" (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k5_pencil_1 :::"Segre_Product"::: ) "A" ")" ) "st" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) "B2") & (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r1_pencil_1 :::"are_collinear"::: ) ) ")" ))); end; :: deftheorem defines :::"'||'"::: PENCIL_3:def 2 : (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#v15_pencil_1 :::"PLS-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "B1")) "," (Set (Var "B2")) "being" ($#m1_pencil_2 :::"Segre-Coset"::: ) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "B1")) ($#r1_pencil_3 :::"'||'"::: ) (Set (Var "B2"))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k5_pencil_1 :::"Segre_Product"::: ) (Set (Var "A")) ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "B1")))) "holds" (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k5_pencil_1 :::"Segre_Product"::: ) (Set (Var "A")) ")" ) "st" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "B2"))) & (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r1_pencil_1 :::"are_collinear"::: ) ) ")" ))) ")" )))); theorem :: PENCIL_3:20 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#v15_pencil_1 :::"PLS-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "B1")) "," (Set (Var "B2")) "being" ($#m1_pencil_2 :::"Segre-Coset"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "B1")) ($#r1_pencil_3 :::"'||'"::: ) (Set (Var "B2")))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Collineation":::) "of" (Set "(" ($#k5_pencil_1 :::"Segre_Product"::: ) (Set (Var "A")) ")" ) (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_pencil_2 :::"Segre-Coset"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "C1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "B1")))) & (Bool (Set (Var "C2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "B2"))))) "holds" (Bool (Set (Var "C1")) ($#r1_pencil_3 :::"'||'"::: ) (Set (Var "C2")))))))) ; theorem :: PENCIL_3:21 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#v15_pencil_1 :::"PLS-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "B1")) "," (Set (Var "B2")) "being" ($#m1_pencil_2 :::"Segre-Coset"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "B1")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B2")))) "holds" (Bool "(" (Bool (Set (Var "B1")) ($#r1_pencil_3 :::"'||'"::: ) (Set (Var "B2"))) "iff" (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#~v13_pencil_1 "non" ($#v13_pencil_1 :::"trivial-yielding"::: ) ) ($#v16_pencil_1 :::"Segre-like"::: ) ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set ($#k12_pralg_1 :::"Carrier"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "B1")) ($#r1_hidden :::"="::: ) (Set ($#k4_card_3 :::"product"::: ) (Set (Var "b1")))) & (Bool (Set (Var "B2")) ($#r1_hidden :::"="::: ) (Set ($#k4_card_3 :::"product"::: ) (Set (Var "b2"))))) "holds" (Bool "(" (Bool (Set ($#k3_pencil_1 :::"indx"::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_pencil_1 :::"indx"::: ) (Set (Var "b2")))) & (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) "st" (Bool "(" (Bool (Set (Var "r")) ($#r1_hidden :::"<>"::: ) (Set ($#k3_pencil_1 :::"indx"::: ) (Set (Var "b1")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Var "r")))) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) ")" ) & (Bool "(" "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" (Set (Var "A")) ($#k2_pencil_1 :::"."::: ) (Set (Var "r")) ")" ) "st" (Bool (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "c1")) ($#k6_domain_1 :::"}"::: ) )) & (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "c2")) ($#k6_domain_1 :::"}"::: ) ))) "holds" (Bool (Set (Var "c1")) "," (Set (Var "c2")) ($#r1_pencil_1 :::"are_collinear"::: ) ) ")" ) ")" )) ")" )) ")" )))) ; theorem :: PENCIL_3:22 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#v15_pencil_1 :::"PLS-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "A")) ($#k2_pencil_1 :::"."::: ) (Set (Var "i"))) "is" ($#v9_pencil_1 :::"connected"::: ) ) ")" )) "holds" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" (Set (Var "A")) ($#k2_pencil_1 :::"."::: ) (Set (Var "i")) ")" ) (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#~v13_pencil_1 "non" ($#v13_pencil_1 :::"trivial-yielding"::: ) ) ($#v16_pencil_1 :::"Segre-like"::: ) ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set ($#k12_pralg_1 :::"Carrier"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set ($#k4_card_3 :::"product"::: ) (Set (Var "b2"))) "is" ($#m1_pencil_2 :::"Segre-Coset"::: ) "of" (Set (Var "A"))) & (Bool (Set (Var "b1")) ($#r8_pboole :::"="::: ) (Set (Set (Var "b2")) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "p")) ($#k6_domain_1 :::"}"::: ) ) ")" )) & (Bool (Bool "not" (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))))) "holds" (Bool "ex" (Set (Var "D")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k5_pencil_1 :::"Segre_Product"::: ) (Set (Var "A")) ")" ))) "st" (Bool "(" (Bool (Set (Set (Var "D")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k4_card_3 :::"product"::: ) (Set (Var "b1")))) & (Bool (Set (Set (Var "D")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "D")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_card_3 :::"product"::: ) (Set (Var "b2")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "D"))))) "holds" (Bool (Set (Set (Var "D")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) "is" ($#m1_pencil_2 :::"Segre-Coset"::: ) "of" (Set (Var "A"))) ")" ) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "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 "D"))))) "holds" (Bool "for" (Set (Var "Di")) "," (Set (Var "Di1")) "being" ($#m1_pencil_2 :::"Segre-Coset"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "Di")) ($#r1_hidden :::"="::: ) (Set (Set (Var "D")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "Di1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "D")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )))) "holds" (Bool "(" (Bool (Set (Var "Di")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "Di1"))) & (Bool (Set (Var "Di")) ($#r1_pencil_3 :::"'||'"::: ) (Set (Var "Di1"))) ")" )) ")" ) ")" ))))))) ; theorem :: PENCIL_3:23 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#v15_pencil_1 :::"PLS-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "A")) ($#k2_pencil_1 :::"."::: ) (Set (Var "i"))) "is" ($#v9_pencil_1 :::"connected"::: ) ) ")" )) "holds" (Bool "for" (Set (Var "B1")) "," (Set (Var "B2")) "being" ($#m1_pencil_2 :::"Segre-Coset"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "B1")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B2")))) "holds" (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#~v13_pencil_1 "non" ($#v13_pencil_1 :::"trivial-yielding"::: ) ) ($#v16_pencil_1 :::"Segre-like"::: ) ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set ($#k12_pralg_1 :::"Carrier"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "B1")) ($#r1_hidden :::"="::: ) (Set ($#k4_card_3 :::"product"::: ) (Set (Var "b1")))) & (Bool (Set (Var "B2")) ($#r1_hidden :::"="::: ) (Set ($#k4_card_3 :::"product"::: ) (Set (Var "b2"))))) "holds" (Bool "(" (Bool (Set ($#k3_pencil_1 :::"indx"::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_pencil_1 :::"indx"::: ) (Set (Var "b2")))) "iff" (Bool "ex" (Set (Var "D")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k5_pencil_1 :::"Segre_Product"::: ) (Set (Var "A")) ")" ))) "st" (Bool "(" (Bool (Set (Set (Var "D")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "B1"))) & (Bool (Set (Set (Var "D")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "D")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "B2"))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "D"))))) "holds" (Bool (Set (Set (Var "D")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) "is" ($#m1_pencil_2 :::"Segre-Coset"::: ) "of" (Set (Var "A"))) ")" ) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "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 "D"))))) "holds" (Bool "for" (Set (Var "Di")) "," (Set (Var "Di1")) "being" ($#m1_pencil_2 :::"Segre-Coset"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "Di")) ($#r1_hidden :::"="::: ) (Set (Set (Var "D")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "Di1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "D")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )))) "holds" (Bool "(" (Bool (Set (Var "Di")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "Di1"))) & (Bool (Set (Var "Di")) ($#r1_pencil_3 :::"'||'"::: ) (Set (Var "Di1"))) ")" )) ")" ) ")" )) ")" ))))) ; theorem :: PENCIL_3:24 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#v15_pencil_1 :::"PLS-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "A")) ($#k2_pencil_1 :::"."::: ) (Set (Var "i"))) "is" ($#v10_pencil_1 :::"strongly_connected"::: ) ) ")" )) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Collineation":::) "of" (Set "(" ($#k5_pencil_1 :::"Segre_Product"::: ) (Set (Var "A")) ")" ) (Bool "for" (Set (Var "B1")) "," (Set (Var "B2")) "being" ($#m1_pencil_2 :::"Segre-Coset"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "b3")) "," (Set (Var "b4")) "being" ($#~v13_pencil_1 "non" ($#v13_pencil_1 :::"trivial-yielding"::: ) ) ($#v16_pencil_1 :::"Segre-like"::: ) ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set ($#k12_pralg_1 :::"Carrier"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "B1")) ($#r1_hidden :::"="::: ) (Set ($#k4_card_3 :::"product"::: ) (Set (Var "b1")))) & (Bool (Set (Var "B2")) ($#r1_hidden :::"="::: ) (Set ($#k4_card_3 :::"product"::: ) (Set (Var "b2")))) & (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "B1"))) ($#r1_hidden :::"="::: ) (Set ($#k4_card_3 :::"product"::: ) (Set (Var "b3")))) & (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "B2"))) ($#r1_hidden :::"="::: ) (Set ($#k4_card_3 :::"product"::: ) (Set (Var "b4")))) & (Bool (Set ($#k3_pencil_1 :::"indx"::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_pencil_1 :::"indx"::: ) (Set (Var "b2"))))) "holds" (Bool (Set ($#k3_pencil_1 :::"indx"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k3_pencil_1 :::"indx"::: ) (Set (Var "b4"))))))))) ; theorem :: PENCIL_3:25 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#v15_pencil_1 :::"PLS-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "A")) ($#k2_pencil_1 :::"."::: ) (Set (Var "i"))) "is" ($#v10_pencil_1 :::"strongly_connected"::: ) ) ")" )) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Collineation":::) "of" (Set "(" ($#k5_pencil_1 :::"Segre_Product"::: ) (Set (Var "A")) ")" ) (Bool "ex" (Set (Var "s")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set (Var "I")) "st" (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Set (Var "s")) ($#k3_funct_2 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Var "j"))) "iff" (Bool "for" (Set (Var "B1")) "being" ($#m1_pencil_2 :::"Segre-Coset"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#~v13_pencil_1 "non" ($#v13_pencil_1 :::"trivial-yielding"::: ) ) ($#v16_pencil_1 :::"Segre-like"::: ) ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set ($#k12_pralg_1 :::"Carrier"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "B1")) ($#r1_hidden :::"="::: ) (Set ($#k4_card_3 :::"product"::: ) (Set (Var "b1")))) & (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "B1"))) ($#r1_hidden :::"="::: ) (Set ($#k4_card_3 :::"product"::: ) (Set (Var "b2")))) & (Bool (Set ($#k3_pencil_1 :::"indx"::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set (Var "i")))) "holds" (Bool (Set ($#k3_pencil_1 :::"indx"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set (Var "j"))))) ")" )))))) ; definitionlet "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; let "A" be ($#v15_pencil_1 :::"PLS-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); assume (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "I")) "holds" (Bool (Set (Set (Const "A")) ($#k2_pencil_1 :::"."::: ) (Set (Var "i"))) "is" ($#v10_pencil_1 :::"strongly_connected"::: ) )) ; let "f" be ($#m1_subset_1 :::"Collineation":::) "of" (Set "(" ($#k5_pencil_1 :::"Segre_Product"::: ) (Set (Const "A")) ")" ); func :::"permutation_of_indices"::: "f" -> ($#m1_subset_1 :::"Permutation":::) "of" "I" means :: PENCIL_3:def 3 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "I" "holds" (Bool "(" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Var "j"))) "iff" (Bool "for" (Set (Var "B1")) "being" ($#m1_pencil_2 :::"Segre-Coset"::: ) "of" "A" (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#~v13_pencil_1 "non" ($#v13_pencil_1 :::"trivial-yielding"::: ) ) ($#v16_pencil_1 :::"Segre-like"::: ) ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set ($#k12_pralg_1 :::"Carrier"::: ) "A") "st" (Bool (Bool (Set (Var "B1")) ($#r1_hidden :::"="::: ) (Set ($#k4_card_3 :::"product"::: ) (Set (Var "b1")))) & (Bool (Set "f" ($#k7_relset_1 :::".:"::: ) (Set (Var "B1"))) ($#r1_hidden :::"="::: ) (Set ($#k4_card_3 :::"product"::: ) (Set (Var "b2")))) & (Bool (Set ($#k3_pencil_1 :::"indx"::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set (Var "i")))) "holds" (Bool (Set ($#k3_pencil_1 :::"indx"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set (Var "j"))))) ")" )); end; :: deftheorem defines :::"permutation_of_indices"::: PENCIL_3:def 3 : (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#v15_pencil_1 :::"PLS-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "A")) ($#k2_pencil_1 :::"."::: ) (Set (Var "i"))) "is" ($#v10_pencil_1 :::"strongly_connected"::: ) ) ")" )) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Collineation":::) "of" (Set "(" ($#k5_pencil_1 :::"Segre_Product"::: ) (Set (Var "A")) ")" ) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k2_pencil_3 :::"permutation_of_indices"::: ) (Set (Var "f")))) "iff" (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Set (Var "b4")) ($#k3_funct_2 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Var "j"))) "iff" (Bool "for" (Set (Var "B1")) "being" ($#m1_pencil_2 :::"Segre-Coset"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#~v13_pencil_1 "non" ($#v13_pencil_1 :::"trivial-yielding"::: ) ) ($#v16_pencil_1 :::"Segre-like"::: ) ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set ($#k12_pralg_1 :::"Carrier"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "B1")) ($#r1_hidden :::"="::: ) (Set ($#k4_card_3 :::"product"::: ) (Set (Var "b1")))) & (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "B1"))) ($#r1_hidden :::"="::: ) (Set ($#k4_card_3 :::"product"::: ) (Set (Var "b2")))) & (Bool (Set ($#k3_pencil_1 :::"indx"::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set (Var "i")))) "holds" (Bool (Set ($#k3_pencil_1 :::"indx"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set (Var "j"))))) ")" )) ")" ))))); begin definitionlet "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; let "A" be ($#v15_pencil_1 :::"PLS-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); assume (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "I")) "holds" (Bool (Set (Set (Const "A")) ($#k2_pencil_1 :::"."::: ) (Set (Var "i"))) "is" ($#v10_pencil_1 :::"strongly_connected"::: ) )) ; let "f" be ($#m1_subset_1 :::"Collineation":::) "of" (Set "(" ($#k5_pencil_1 :::"Segre_Product"::: ) (Set (Const "A")) ")" ); let "b1" be ($#~v13_pencil_1 "non" ($#v13_pencil_1 :::"trivial-yielding"::: ) ) ($#v16_pencil_1 :::"Segre-like"::: ) ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set ($#k12_pralg_1 :::"Carrier"::: ) (Set (Const "A"))); assume (Bool (Set ($#k4_card_3 :::"product"::: ) (Set (Const "b1"))) "is" ($#m1_pencil_2 :::"Segre-Coset"::: ) "of" (Set (Const "A"))) ; func :::"canonical_embedding"::: "(" "f" "," "b1" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" "A" ($#k2_pencil_1 :::"."::: ) (Set "(" ($#k3_pencil_1 :::"indx"::: ) "b1" ")" ) ")" ) "," (Set "(" "A" ($#k2_pencil_1 :::"."::: ) (Set "(" (Set "(" ($#k2_pencil_3 :::"permutation_of_indices"::: ) "f" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k3_pencil_1 :::"indx"::: ) "b1" ")" ) ")" ) ")" ) means :: PENCIL_3:def 4 (Bool "(" (Bool it "is" ($#v1_pencil_2 :::"isomorphic"::: ) ) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" "I" "st" (Bool (Bool (Set (Var "a")) "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k5_pencil_1 :::"Segre_Product"::: ) "A" ")" )) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k4_card_3 :::"product"::: ) "b1"))) "holds" (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" "I" "st" (Bool (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "a"))))) "holds" (Bool (Set (Set (Var "b")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k2_pencil_3 :::"permutation_of_indices"::: ) "f" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k3_pencil_1 :::"indx"::: ) "b1" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set it ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "a")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_pencil_1 :::"indx"::: ) "b1" ")" ) ")" )))) ")" ) ")" ); end; :: deftheorem defines :::"canonical_embedding"::: PENCIL_3:def 4 : (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#v15_pencil_1 :::"PLS-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "A")) ($#k2_pencil_1 :::"."::: ) (Set (Var "i"))) "is" ($#v10_pencil_1 :::"strongly_connected"::: ) ) ")" )) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Collineation":::) "of" (Set "(" ($#k5_pencil_1 :::"Segre_Product"::: ) (Set (Var "A")) ")" ) (Bool "for" (Set (Var "b1")) "being" ($#~v13_pencil_1 "non" ($#v13_pencil_1 :::"trivial-yielding"::: ) ) ($#v16_pencil_1 :::"Segre-like"::: ) ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set ($#k12_pralg_1 :::"Carrier"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set ($#k4_card_3 :::"product"::: ) (Set (Var "b1"))) "is" ($#m1_pencil_2 :::"Segre-Coset"::: ) "of" (Set (Var "A")))) "holds" (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "A")) ($#k2_pencil_1 :::"."::: ) (Set "(" ($#k3_pencil_1 :::"indx"::: ) (Set (Var "b1")) ")" ) ")" ) "," (Set "(" (Set (Var "A")) ($#k2_pencil_1 :::"."::: ) (Set "(" (Set "(" ($#k2_pencil_3 :::"permutation_of_indices"::: ) (Set (Var "f")) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k3_pencil_1 :::"indx"::: ) (Set (Var "b1")) ")" ) ")" ) ")" ) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k3_pencil_3 :::"canonical_embedding"::: ) "(" (Set (Var "f")) "," (Set (Var "b1")) ")" )) "iff" (Bool "(" (Bool (Set (Var "b5")) "is" ($#v1_pencil_2 :::"isomorphic"::: ) ) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "a")) "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k5_pencil_1 :::"Segre_Product"::: ) (Set (Var "A")) ")" )) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k4_card_3 :::"product"::: ) (Set (Var "b1"))))) "holds" (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))))) "holds" (Bool (Set (Set (Var "b")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k2_pencil_3 :::"permutation_of_indices"::: ) (Set (Var "f")) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k3_pencil_1 :::"indx"::: ) (Set (Var "b1")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "b5")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "a")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_pencil_1 :::"indx"::: ) (Set (Var "b1")) ")" ) ")" )))) ")" ) ")" ) ")" )))))); theorem :: PENCIL_3:26 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#v15_pencil_1 :::"PLS-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "A")) ($#k2_pencil_1 :::"."::: ) (Set (Var "i"))) "is" ($#v10_pencil_1 :::"strongly_connected"::: ) ) ")" )) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Collineation":::) "of" (Set "(" ($#k5_pencil_1 :::"Segre_Product"::: ) (Set (Var "A")) ")" ) (Bool "for" (Set (Var "B1")) "," (Set (Var "B2")) "being" ($#m1_pencil_2 :::"Segre-Coset"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "B1")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B2"))) & (Bool (Set (Var "B1")) ($#r1_pencil_3 :::"'||'"::: ) (Set (Var "B2")))) "holds" (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#~v13_pencil_1 "non" ($#v13_pencil_1 :::"trivial-yielding"::: ) ) ($#v16_pencil_1 :::"Segre-like"::: ) ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set ($#k12_pralg_1 :::"Carrier"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set ($#k4_card_3 :::"product"::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set (Var "B1"))) & (Bool (Set ($#k4_card_3 :::"product"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set (Var "B2")))) "holds" (Bool (Set ($#k3_pencil_3 :::"canonical_embedding"::: ) "(" (Set (Var "f")) "," (Set (Var "b1")) ")" ) ($#r1_funct_2 :::"="::: ) (Set ($#k3_pencil_3 :::"canonical_embedding"::: ) "(" (Set (Var "f")) "," (Set (Var "b2")) ")" ))))))) ; theorem :: PENCIL_3:27 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#v15_pencil_1 :::"PLS-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "A")) ($#k2_pencil_1 :::"."::: ) (Set (Var "i"))) "is" ($#v10_pencil_1 :::"strongly_connected"::: ) ) ")" )) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Collineation":::) "of" (Set "(" ($#k5_pencil_1 :::"Segre_Product"::: ) (Set (Var "A")) ")" ) (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#~v13_pencil_1 "non" ($#v13_pencil_1 :::"trivial-yielding"::: ) ) ($#v16_pencil_1 :::"Segre-like"::: ) ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set ($#k12_pralg_1 :::"Carrier"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set ($#k4_card_3 :::"product"::: ) (Set (Var "b1"))) "is" ($#m1_pencil_2 :::"Segre-Coset"::: ) "of" (Set (Var "A"))) & (Bool (Set ($#k4_card_3 :::"product"::: ) (Set (Var "b2"))) "is" ($#m1_pencil_2 :::"Segre-Coset"::: ) "of" (Set (Var "A"))) & (Bool (Set ($#k3_pencil_1 :::"indx"::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_pencil_1 :::"indx"::: ) (Set (Var "b2"))))) "holds" (Bool (Set ($#k3_pencil_3 :::"canonical_embedding"::: ) "(" (Set (Var "f")) "," (Set (Var "b1")) ")" ) ($#r1_funct_2 :::"="::: ) (Set ($#k3_pencil_3 :::"canonical_embedding"::: ) "(" (Set (Var "f")) "," (Set (Var "b2")) ")" )))))) ; definitionlet "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; let "A" be ($#v15_pencil_1 :::"PLS-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); assume (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "I")) "holds" (Bool (Set (Set (Const "A")) ($#k2_pencil_1 :::"."::: ) (Set (Var "i"))) "is" ($#v10_pencil_1 :::"strongly_connected"::: ) )) ; let "f" be ($#m1_subset_1 :::"Collineation":::) "of" (Set "(" ($#k5_pencil_1 :::"Segre_Product"::: ) (Set (Const "A")) ")" ); let "i" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "I")); func :::"canonical_embedding"::: "(" "f" "," "i" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" "A" ($#k2_pencil_1 :::"."::: ) "i" ")" ) "," (Set "(" "A" ($#k2_pencil_1 :::"."::: ) (Set "(" (Set "(" ($#k2_pencil_3 :::"permutation_of_indices"::: ) "f" ")" ) ($#k3_funct_2 :::"."::: ) "i" ")" ) ")" ) means :: PENCIL_3:def 5 (Bool "for" (Set (Var "b")) "being" ($#~v13_pencil_1 "non" ($#v13_pencil_1 :::"trivial-yielding"::: ) ) ($#v16_pencil_1 :::"Segre-like"::: ) ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set ($#k12_pralg_1 :::"Carrier"::: ) "A") "st" (Bool (Bool (Set ($#k4_card_3 :::"product"::: ) (Set (Var "b"))) "is" ($#m1_pencil_2 :::"Segre-Coset"::: ) "of" "A") & (Bool (Set ($#k3_pencil_1 :::"indx"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) "i")) "holds" (Bool it ($#r1_funct_2 :::"="::: ) (Set ($#k3_pencil_3 :::"canonical_embedding"::: ) "(" "f" "," (Set (Var "b")) ")" ))); end; :: deftheorem defines :::"canonical_embedding"::: PENCIL_3:def 5 : (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#v15_pencil_1 :::"PLS-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "A")) ($#k2_pencil_1 :::"."::: ) (Set (Var "i"))) "is" ($#v10_pencil_1 :::"strongly_connected"::: ) ) ")" )) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Collineation":::) "of" (Set "(" ($#k5_pencil_1 :::"Segre_Product"::: ) (Set (Var "A")) ")" ) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "A")) ($#k2_pencil_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "A")) ($#k2_pencil_1 :::"."::: ) (Set "(" (Set "(" ($#k2_pencil_3 :::"permutation_of_indices"::: ) (Set (Var "f")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "i")) ")" ) ")" ) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k4_pencil_3 :::"canonical_embedding"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) ")" )) "iff" (Bool "for" (Set (Var "b")) "being" ($#~v13_pencil_1 "non" ($#v13_pencil_1 :::"trivial-yielding"::: ) ) ($#v16_pencil_1 :::"Segre-like"::: ) ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set ($#k12_pralg_1 :::"Carrier"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set ($#k4_card_3 :::"product"::: ) (Set (Var "b"))) "is" ($#m1_pencil_2 :::"Segre-Coset"::: ) "of" (Set (Var "A"))) & (Bool (Set ($#k3_pencil_1 :::"indx"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Var "i")))) "holds" (Bool (Set (Var "b5")) ($#r1_funct_2 :::"="::: ) (Set ($#k3_pencil_3 :::"canonical_embedding"::: ) "(" (Set (Var "f")) "," (Set (Var "b")) ")" ))) ")" )))))); theorem :: PENCIL_3:28 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#v15_pencil_1 :::"PLS-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "A")) ($#k2_pencil_1 :::"."::: ) (Set (Var "i"))) "is" ($#v10_pencil_1 :::"strongly_connected"::: ) ) ")" )) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Collineation":::) "of" (Set "(" ($#k5_pencil_1 :::"Segre_Product"::: ) (Set (Var "A")) ")" ) (Bool "ex" (Set (Var "s")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set (Var "I"))(Bool "ex" (Set (Var "B")) "being" ($#v1_funcop_1 :::"Function-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Set (Var "B")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) "is" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "A")) ($#k2_pencil_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "A")) ($#k2_pencil_1 :::"."::: ) (Set "(" (Set (Var "s")) ($#k3_funct_2 :::"."::: ) (Set (Var "i")) ")" ) ")" )) & (Bool "(" "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "A")) ($#k2_pencil_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "A")) ($#k2_pencil_1 :::"."::: ) (Set "(" (Set (Var "s")) ($#k3_funct_2 :::"."::: ) (Set (Var "i")) ")" ) ")" ) "st" (Bool (Bool (Set (Var "m")) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool (Set (Var "m")) "is" ($#v1_pencil_2 :::"isomorphic"::: ) ) ")" ) & (Bool "(" "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k5_pencil_1 :::"Segre_Product"::: ) (Set (Var "A")) ")" ) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "p")))) "holds" (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))))) "holds" (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "A")) ($#k2_pencil_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "A")) ($#k2_pencil_1 :::"."::: ) (Set "(" (Set (Var "s")) ($#k3_funct_2 :::"."::: ) (Set (Var "i")) ")" ) ")" ) "st" (Bool (Bool (Set (Var "m")) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool (Set (Set (Var "b")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "s")) ($#k3_funct_2 :::"."::: ) (Set (Var "i")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "m")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "a")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" )))))) ")" ) ")" ))))))) ;