:: PENCIL_2 semantic presentation begin definitionlet "D" be ($#m1_hidden :::"set"::: ) ; let "p" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "D")); let "i", "j" be ($#m1_hidden :::"Nat":::); func :::"Del"::: "(" "p" "," "i" "," "j" ")" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" "D" equals :: PENCIL_2:def 1 (Set (Set "(" "p" ($#k17_finseq_1 :::"|"::: ) (Set "(" "i" ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" "p" ($#k2_rfinseq :::"/^"::: ) "j" ")" )); end; :: deftheorem defines :::"Del"::: PENCIL_2:def 1 : (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k1_pencil_2 :::"Del"::: ) "(" (Set (Var "p")) "," (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k17_finseq_1 :::"|"::: ) (Set "(" (Set (Var "i")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" (Set (Var "p")) ($#k2_rfinseq :::"/^"::: ) (Set (Var "j")) ")" )))))); theorem :: PENCIL_2:1 (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" ($#k1_pencil_2 :::"Del"::: ) "(" (Set (Var "p")) "," (Set (Var "i")) "," (Set (Var "j")) ")" ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "p"))))))) ; theorem :: PENCIL_2:2 (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_pencil_2 :::"Del"::: ) "(" (Set (Var "p")) "," (Set (Var "i")) "," (Set (Var "j")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "j")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "i")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1)))))) ; theorem :: PENCIL_2:3 (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_pencil_2 :::"Del"::: ) "(" (Set (Var "p")) "," (Set (Var "i")) "," (Set (Var "j")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Var "j")) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")))) ")" )))) ; theorem :: PENCIL_2:4 (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "i")) ($#k6_xcmplx_0 :::"-"::: ) (Num 1)))) "holds" (Bool (Set (Set "(" ($#k1_pencil_2 :::"Del"::: ) "(" (Set (Var "p")) "," (Set (Var "i")) "," (Set (Var "j")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))))))) ; theorem :: PENCIL_2:5 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k")))) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ")" ))))) ; theorem :: PENCIL_2:6 (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "j")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "i")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1)))) "holds" (Bool (Set (Set "(" ($#k1_pencil_2 :::"Del"::: ) "(" (Set (Var "p")) "," (Set (Var "i")) "," (Set (Var "j")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" (Set "(" (Set (Var "j")) ($#k7_nat_d :::"-'"::: ) (Set (Var "i")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "k")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )))))) ; scheme :: PENCIL_2:sch 1 FinSeqOneToOne{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"set"::: ) , F3() -> ($#m1_hidden :::"set"::: ) , F4() -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set F3 "(" ")" ), P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ] } : (Bool "ex" (Set (Var "g")) "being" ($#v2_funct_1 :::"one-to-one"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set F3 "(" ")" ) "st" (Bool "(" (Bool (Set F1 "(" ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Num 1))) & (Bool (Set F2 "(" ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "g")) ")" ))) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "g"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set F4 "(" ")" ))) & (Bool "(" "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "g"))))) "holds" (Bool P1[(Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) "," (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))]) ")" ) ")" )) provided (Bool "(" (Bool (Set F1 "(" ")" ) ($#r1_hidden :::"="::: ) (Set (Set F4 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Num 1))) & (Bool (Set F2 "(" ")" ) ($#r1_hidden :::"="::: ) (Set (Set F4 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set F4 "(" ")" ) ")" ))) ")" ) and (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set F4 "(" ")" ))) & (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set (Set F4 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "d2")) ($#r1_hidden :::"="::: ) (Set (Set F4 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )))) "holds" (Bool P1[(Set (Var "d1")) "," (Set (Var "d2"))]))) proof end; begin theorem :: PENCIL_2: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 "L")) "being" ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set ($#k12_pralg_1 :::"Carrier"::: ) (Set (Var "A"))) (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")) ($#k10_pralg_1 :::"."::: ) (Set (Var "i")) ")" ) "holds" (Bool (Set (Set (Var "L")) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set (Var "S")) ")" ) "is" ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set ($#k12_pralg_1 :::"Carrier"::: ) (Set (Var "A"))))))))) ; definitionlet "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "A" be ($#v11_pencil_1 :::"TopStruct-yielding"::: ) ($#v14_pencil_1 :::"non-Trivial-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); mode :::"Segre-Coset"::: "of" "A" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k5_pencil_1 :::"Segre_Product"::: ) "A" ")" ) means :: PENCIL_2:def 2 (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"::: ) "A") "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set ($#k4_card_3 :::"product"::: ) (Set (Var "L")))) & (Bool (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_pencil_1 :::"indx"::: ) (Set (Var "L")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set "(" "A" ($#k1_pencil_1 :::"."::: ) (Set "(" ($#k3_pencil_1 :::"indx"::: ) (Set (Var "L")) ")" ) ")" ))) ")" )); end; :: deftheorem defines :::"Segre-Coset"::: PENCIL_2: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" ($#v11_pencil_1 :::"TopStruct-yielding"::: ) ($#v14_pencil_1 :::"non-Trivial-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k5_pencil_1 :::"Segre_Product"::: ) (Set (Var "A")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m1_pencil_2 :::"Segre-Coset"::: ) "of" (Set (Var "A"))) "iff" (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 (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k4_card_3 :::"product"::: ) (Set (Var "L")))) & (Bool (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_pencil_1 :::"indx"::: ) (Set (Var "L")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set "(" (Set (Var "A")) ($#k1_pencil_1 :::"."::: ) (Set "(" ($#k3_pencil_1 :::"indx"::: ) (Set (Var "L")) ")" ) ")" ))) ")" )) ")" )))); theorem :: PENCIL_2:8 (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 "B1")) "," (Set (Var "B2")) "being" ($#m1_pencil_2 :::"Segre-Coset"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Num 2) ($#r1_tarski :::"c="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "(" (Set (Var "B1")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B2")) ")" )))) "holds" (Bool (Set (Var "B1")) ($#r1_hidden :::"="::: ) (Set (Var "B2")))))) ; definitionlet "S" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "X", "Y" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "S")); pred "X" "," "Y" :::"are_joinable"::: means :: PENCIL_2:def 3 (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S")) "st" (Bool "(" (Bool "X" ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Num 1))) & (Bool "Y" ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ))) & (Bool "(" "for" (Set (Var "W")) "being" ($#m1_subset_1 :::"Subset":::) "of" "S" "st" (Bool (Bool (Set (Var "W")) ($#r2_hidden :::"in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))))) "holds" (Bool "(" (Bool (Set (Var "W")) "is" ($#v1_pencil_1 :::"closed_under_lines"::: ) ) & (Bool (Set (Var "W")) "is" ($#v2_pencil_1 :::"strong"::: ) ) ")" ) ")" ) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"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 "f"))))) "holds" (Bool (Num 2) ($#r1_tarski :::"c="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ))) ")" ) ")" )); end; :: deftheorem defines :::"are_joinable"::: PENCIL_2:def 3 : (Bool "for" (Set (Var "S")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "X")) "," (Set (Var "Y")) ($#r1_pencil_2 :::"are_joinable"::: ) ) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) "st" (Bool "(" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Num 1))) & (Bool (Set (Var "Y")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ))) & (Bool "(" "for" (Set (Var "W")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "W")) ($#r2_hidden :::"in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))))) "holds" (Bool "(" (Bool (Set (Var "W")) "is" ($#v1_pencil_1 :::"closed_under_lines"::: ) ) & (Bool (Set (Var "W")) "is" ($#v2_pencil_1 :::"strong"::: ) ) ")" ) ")" ) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"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 "f"))))) "holds" (Bool (Num 2) ($#r1_tarski :::"c="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ))) ")" ) ")" )) ")" ))); theorem :: PENCIL_2:9 (Bool "for" (Set (Var "S")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "X")) "," (Set (Var "Y")) ($#r1_pencil_2 :::"are_joinable"::: ) )) "holds" (Bool "ex" (Set (Var "f")) "being" ($#v2_funct_1 :::"one-to-one"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) "st" (Bool "(" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Num 1))) & (Bool (Set (Var "Y")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ))) & (Bool "(" "for" (Set (Var "W")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "W")) ($#r2_hidden :::"in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))))) "holds" (Bool "(" (Bool (Set (Var "W")) "is" ($#v1_pencil_1 :::"closed_under_lines"::: ) ) & (Bool (Set (Var "W")) "is" ($#v2_pencil_1 :::"strong"::: ) ) ")" ) ")" ) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"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 "f"))))) "holds" (Bool (Num 2) ($#r1_tarski :::"c="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ))) ")" ) ")" )))) ; theorem :: PENCIL_2:10 (Bool "for" (Set (Var "S")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_pencil_1 :::"closed_under_lines"::: ) ) & (Bool (Set (Var "X")) "is" ($#v2_pencil_1 :::"strong"::: ) )) "holds" (Bool (Set (Var "X")) "," (Set (Var "X")) ($#r1_pencil_2 :::"are_joinable"::: ) ))) ; theorem :: PENCIL_2:11 (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 "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k5_pencil_1 :::"Segre_Product"::: ) (Set (Var "A")) ")" ) "st" (Bool (Bool (Bool "not" (Set (Var "X")) "is" ($#v1_zfmisc_1 :::"trivial"::: ) )) & (Bool (Set (Var "X")) "is" ($#v1_pencil_1 :::"closed_under_lines"::: ) ) & (Bool (Set (Var "X")) "is" ($#v2_pencil_1 :::"strong"::: ) ) & (Bool (Bool "not" (Set (Var "Y")) "is" ($#v1_zfmisc_1 :::"trivial"::: ) )) & (Bool (Set (Var "Y")) "is" ($#v1_pencil_1 :::"closed_under_lines"::: ) ) & (Bool (Set (Var "Y")) "is" ($#v2_pencil_1 :::"strong"::: ) ) & (Bool (Set (Var "X")) "," (Set (Var "Y")) ($#r1_pencil_2 :::"are_joinable"::: ) )) "holds" (Bool "for" (Set (Var "X1")) "," (Set (Var "Y1")) "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 "X")) ($#r1_hidden :::"="::: ) (Set ($#k4_card_3 :::"product"::: ) (Set (Var "X1")))) & (Bool (Set (Var "Y")) ($#r1_hidden :::"="::: ) (Set ($#k4_card_3 :::"product"::: ) (Set (Var "Y1"))))) "holds" (Bool "(" (Bool (Set ($#k3_pencil_1 :::"indx"::: ) (Set (Var "X1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_pencil_1 :::"indx"::: ) (Set (Var "Y1")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set ($#k3_pencil_1 :::"indx"::: ) (Set (Var "X1"))))) "holds" (Bool (Set (Set (Var "X1")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "Y1")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) ")" ) ")" ))))) ; begin theorem :: PENCIL_2:12 (Bool "for" (Set (Var "S")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v3_funct_2 :::"bijective"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k2_tops_2 :::"""::: ) ) "is" ($#v3_funct_2 :::"bijective"::: ) )))) ; definitionlet "S", "T" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "S")) "," (Set (Const "T")); attr "f" is :::"isomorphic"::: means :: PENCIL_2:def 4 (Bool "(" (Bool "f" "is" ($#v3_funct_2 :::"bijective"::: ) ) & (Bool "f" "is" ($#v1_t_0topsp :::"open"::: ) ) & (Bool (Set "f" ($#k2_tops_2 :::"""::: ) ) "is" ($#v3_funct_2 :::"bijective"::: ) ) & (Bool (Set "f" ($#k2_tops_2 :::"""::: ) ) "is" ($#v1_t_0topsp :::"open"::: ) ) ")" ); end; :: deftheorem defines :::"isomorphic"::: PENCIL_2:def 4 : (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v1_pencil_2 :::"isomorphic"::: ) ) "iff" (Bool "(" (Bool (Set (Var "f")) "is" ($#v3_funct_2 :::"bijective"::: ) ) & (Bool (Set (Var "f")) "is" ($#v1_t_0topsp :::"open"::: ) ) & (Bool (Set (Set (Var "f")) ($#k2_tops_2 :::"""::: ) ) "is" ($#v3_funct_2 :::"bijective"::: ) ) & (Bool (Set (Set (Var "f")) ($#k2_tops_2 :::"""::: ) ) "is" ($#v1_t_0topsp :::"open"::: ) ) ")" ) ")" ))); registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_partfun1 :::"total"::: ) ($#v1_funct_2 :::"quasi_total"::: ) ($#v1_pencil_2 :::"isomorphic"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ($#k2_zfmisc_1 :::":]"::: ) )); end; definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) ; mode Collineation of "S" is ($#v1_pencil_2 :::"isomorphic"::: ) ($#m1_subset_1 :::"Function":::) "of" "S" "," "S"; end; definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v3_pencil_1 "non" ($#v3_pencil_1 :::"void"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) ; let "f" be ($#m1_subset_1 :::"Collineation":::) "of" (Set (Const "S")); let "l" be ($#m1_subset_1 :::"Block":::) "of" (Set (Const "S")); :: original: :::".:"::: redefine func "f" :::".:"::: "l" -> ($#m1_subset_1 :::"Block":::) "of" "S"; end; definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v3_pencil_1 "non" ($#v3_pencil_1 :::"void"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) ; let "f" be ($#m1_subset_1 :::"Collineation":::) "of" (Set (Const "S")); let "l" be ($#m1_subset_1 :::"Block":::) "of" (Set (Const "S")); :: original: :::"""::: redefine func "f" :::"""::: "l" -> ($#m1_subset_1 :::"Block":::) "of" "S"; end; theorem :: PENCIL_2:13 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Collineation":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "f")) ($#k2_tops_2 :::"""::: ) ) "is" ($#m1_subset_1 :::"Collineation":::) "of" (Set (Var "S"))))) ; theorem :: PENCIL_2:14 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Collineation":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "st" (Bool (Bool (Bool "not" (Set (Var "X")) "is" ($#v1_zfmisc_1 :::"trivial"::: ) ))) "holds" (Bool "not" (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "X"))) "is" ($#v1_zfmisc_1 :::"trivial"::: ) ))))) ; theorem :: PENCIL_2:15 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Collineation":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "st" (Bool (Bool (Bool "not" (Set (Var "X")) "is" ($#v1_zfmisc_1 :::"trivial"::: ) ))) "holds" (Bool "not" (Bool (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set (Var "X"))) "is" ($#v1_zfmisc_1 :::"trivial"::: ) ))))) ; theorem :: PENCIL_2:16 (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 "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "X")) "is" ($#v2_pencil_1 :::"strong"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "X"))) "is" ($#v2_pencil_1 :::"strong"::: ) )))) ; theorem :: PENCIL_2:17 (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 "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "X")) "is" ($#v2_pencil_1 :::"strong"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set (Var "X"))) "is" ($#v2_pencil_1 :::"strong"::: ) )))) ; theorem :: PENCIL_2:18 (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 "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_pencil_1 :::"closed_under_lines"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "X"))) "is" ($#v1_pencil_1 :::"closed_under_lines"::: ) )))) ; theorem :: PENCIL_2:19 (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 "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_pencil_1 :::"closed_under_lines"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set (Var "X"))) "is" ($#v1_pencil_1 :::"closed_under_lines"::: ) )))) ; theorem :: PENCIL_2:20 (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 "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "st" (Bool (Bool (Bool "not" (Set (Var "X")) "is" ($#v1_zfmisc_1 :::"trivial"::: ) )) & (Bool (Bool "not" (Set (Var "Y")) "is" ($#v1_zfmisc_1 :::"trivial"::: ) )) & (Bool (Set (Var "X")) "," (Set (Var "Y")) ($#r1_pencil_2 :::"are_joinable"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "X"))) "," (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "Y"))) ($#r1_pencil_2 :::"are_joinable"::: ) )))) ; theorem :: PENCIL_2:21 (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 "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "st" (Bool (Bool (Bool "not" (Set (Var "X")) "is" ($#v1_zfmisc_1 :::"trivial"::: ) )) & (Bool (Bool "not" (Set (Var "Y")) "is" ($#v1_zfmisc_1 :::"trivial"::: ) )) & (Bool (Set (Var "X")) "," (Set (Var "Y")) ($#r1_pencil_2 :::"are_joinable"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set (Var "X"))) "," (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set (Var "Y"))) ($#r1_pencil_2 :::"are_joinable"::: ) )))) ; theorem :: PENCIL_2:22 (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")) "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 "W")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k5_pencil_1 :::"Segre_Product"::: ) (Set (Var "A")) ")" ) "st" (Bool (Bool (Bool "not" (Set (Var "W")) "is" ($#v1_zfmisc_1 :::"trivial"::: ) )) & (Bool (Set (Var "W")) "is" ($#v2_pencil_1 :::"strong"::: ) ) & (Bool (Set (Var "W")) "is" ($#v1_pencil_1 :::"closed_under_lines"::: ) )) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) "{" (Set (Var "Y")) where Y "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k5_pencil_1 :::"Segre_Product"::: ) (Set (Var "A")) ")" ) : (Bool "(" (Bool (Bool "not" (Set (Var "Y")) "is" ($#v1_zfmisc_1 :::"trivial"::: ) )) & (Bool (Set (Var "Y")) "is" ($#v2_pencil_1 :::"strong"::: ) ) & (Bool (Set (Var "Y")) "is" ($#v1_pencil_1 :::"closed_under_lines"::: ) ) & (Bool (Set (Var "W")) "," (Set (Var "Y")) ($#r1_pencil_2 :::"are_joinable"::: ) ) ")" ) "}" ) "is" ($#m1_pencil_2 :::"Segre-Coset"::: ) "of" (Set (Var "A")))))) ; theorem :: PENCIL_2:23 (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")) "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 "B")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "B")) "is" ($#m1_pencil_2 :::"Segre-Coset"::: ) "of" (Set (Var "A"))) "iff" (Bool "ex" (Set (Var "W")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k5_pencil_1 :::"Segre_Product"::: ) (Set (Var "A")) ")" ) "st" (Bool "(" (Bool (Bool "not" (Set (Var "W")) "is" ($#v1_zfmisc_1 :::"trivial"::: ) )) & (Bool (Set (Var "W")) "is" ($#v2_pencil_1 :::"strong"::: ) ) & (Bool (Set (Var "W")) "is" ($#v1_pencil_1 :::"closed_under_lines"::: ) ) & (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set (Var "Y")) where Y "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k5_pencil_1 :::"Segre_Product"::: ) (Set (Var "A")) ")" ) : (Bool "(" (Bool (Bool "not" (Set (Var "Y")) "is" ($#v1_zfmisc_1 :::"trivial"::: ) )) & (Bool (Set (Var "Y")) "is" ($#v2_pencil_1 :::"strong"::: ) ) & (Bool (Set (Var "Y")) "is" ($#v1_pencil_1 :::"closed_under_lines"::: ) ) & (Bool (Set (Var "W")) "," (Set (Var "Y")) ($#r1_pencil_2 :::"are_joinable"::: ) ) ")" ) "}" )) ")" )) ")" )))) ; theorem :: PENCIL_2:24 (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")) "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 "B")) "being" ($#m1_pencil_2 :::"Segre-Coset"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Collineation":::) "of" (Set "(" ($#k5_pencil_1 :::"Segre_Product"::: ) (Set (Var "A")) ")" ) "holds" (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "B"))) "is" ($#m1_pencil_2 :::"Segre-Coset"::: ) "of" (Set (Var "A"))))))) ; theorem :: PENCIL_2:25 (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")) "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 "B")) "being" ($#m1_pencil_2 :::"Segre-Coset"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Collineation":::) "of" (Set "(" ($#k5_pencil_1 :::"Segre_Product"::: ) (Set (Var "A")) ")" ) "holds" (Bool (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set (Var "B"))) "is" ($#m1_pencil_2 :::"Segre-Coset"::: ) "of" (Set (Var "A"))))))) ;