begin
theorem Th1:
theorem Th2:
for
X being
set holds
( 2
c= card X iff ex
x,
y being
set st
(
x in X &
y in X &
x <> y ) )
theorem Th3:
theorem Th4:
theorem Th5:
for
X being
set holds
( 3
c= card X iff ex
x,
y,
z being
set st
(
x in X &
y in X &
z in X &
x <> y &
x <> z &
y <> z ) )
theorem Th6:
begin
:: deftheorem Def1 defines are_collinear PENCIL_1:def 1 :
:: deftheorem Def2 defines closed_under_lines PENCIL_1:def 2 :
:: deftheorem Def3 defines strong PENCIL_1:def 3 :
:: deftheorem Def4 defines void PENCIL_1:def 4 :
:: deftheorem Def5 defines degenerated PENCIL_1:def 5 :
:: deftheorem Def6 defines with_non_trivial_blocks PENCIL_1:def 6 :
:: deftheorem Def7 defines identifying_close_blocks PENCIL_1:def 7 :
:: deftheorem Def8 defines truly-partial PENCIL_1:def 8 :
:: deftheorem Def9 defines without_isolated_points PENCIL_1:def 9 :
:: deftheorem defines connected PENCIL_1:def 10 :
:: deftheorem Def11 defines strongly_connected PENCIL_1:def 11 :
theorem Th7:
Lm1:
ex S being TopStruct st
( S is strict & not S is empty & not S is void & not S is degenerated & not S is truly-partial & S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points )
theorem Th8:
Lm2:
ex S being TopStruct st
( S is strict & not S is empty & not S is void & not S is degenerated & S is truly-partial & S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points )
:: deftheorem defines are_collinear PENCIL_1:def 12 :
:: deftheorem Def13 defines TopStruct-yielding PENCIL_1:def 13 :
:: deftheorem Def14 defines non-void-yielding PENCIL_1:def 14 :
:: deftheorem defines non-void-yielding PENCIL_1:def 15 :
:: deftheorem Def16 defines trivial-yielding PENCIL_1:def 16 :
:: deftheorem Def17 defines non-Trivial-yielding PENCIL_1:def 17 :
:: deftheorem defines non-Trivial-yielding PENCIL_1:def 18 :
:: deftheorem Def19 defines PLS-yielding PENCIL_1:def 19 :
:: deftheorem Def20 defines Segre-like PENCIL_1:def 20 :
theorem
theorem
theorem Th11:
:: deftheorem Def21 defines indx PENCIL_1:def 21 :
theorem Th12:
theorem Th13:
begin
:: deftheorem Def22 defines Segre_Blocks PENCIL_1:def 22 :
:: deftheorem defines Segre_Product PENCIL_1:def 23 :
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem
theorem Th20:
theorem Th21:
theorem
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem
theorem