:: The Class of Series-Parallel Graphs, {III}
:: by Krzysztof Retel
::
:: Received February 3, 2004
:: Copyright (c) 2004 Association of Mizar Users
theorem Th1: :: NECKLA_3:1
theorem :: NECKLA_3:2
for
a,
b,
c,
d being
set holds
id {a,b,c,d} = {[a,a],[b,b],[c,c],[d,d]}
theorem Th3: :: NECKLA_3:3
for
a,
b,
c,
d,
e,
f,
g,
h being
set holds
[:{a,b,c,d},{e,f,g,h}:] = {[a,e],[a,f],[b,e],[b,f],[a,g],[a,h],[b,g],[b,h]} \/ {[c,e],[c,f],[d,e],[d,f],[c,g],[c,h],[d,g],[d,h]}
theorem Th4: :: NECKLA_3:4
theorem Th5: :: NECKLA_3:5
theorem Th6: :: NECKLA_3:6
theorem :: NECKLA_3:7
theorem Th8: :: NECKLA_3:8
theorem Th9: :: NECKLA_3:9
theorem Th10: :: NECKLA_3:10
theorem Th11: :: NECKLA_3:11
the
InternalRel of
(ComplRelStr (Necklace 4)) = {[0 ,2],[2,0 ],[0 ,3],[3,0 ],[1,3],[3,1]}
theorem Th12: :: NECKLA_3:12
theorem Th13: :: NECKLA_3:13
theorem Th14: :: NECKLA_3:14
theorem Th15: :: NECKLA_3:15
theorem Th16: :: NECKLA_3:16
theorem Th17: :: NECKLA_3:17
theorem Th18: :: NECKLA_3:18
theorem :: NECKLA_3:19
theorem Th20: :: NECKLA_3:20
theorem :: NECKLA_3:21
theorem Th22: :: NECKLA_3:22
theorem Th23: :: NECKLA_3:23
theorem Th24: :: NECKLA_3:24
theorem Th25: :: NECKLA_3:25
:: deftheorem Def1 defines path-connected NECKLA_3:def 1 :
theorem Th26: :: NECKLA_3:26
theorem Th27: :: NECKLA_3:27
:: deftheorem Def2 defines path-connected NECKLA_3:def 2 :
:: deftheorem defines component NECKLA_3:def 3 :
theorem :: NECKLA_3:28
canceled;
theorem Th29: :: NECKLA_3:29
theorem Th30: :: NECKLA_3:30
theorem Th31: :: NECKLA_3:31
theorem Th32: :: NECKLA_3:32
Lm1:
for X being non empty finite set
for A, B being non empty set st X = A \/ B & A misses B holds
card A in card X
theorem :: NECKLA_3:33
theorem Th34: :: NECKLA_3:34
theorem :: NECKLA_3:35
theorem Th36: :: NECKLA_3:36
theorem :: NECKLA_3:37
theorem Th38: :: NECKLA_3:38
theorem Th39: :: NECKLA_3:39
for
G being non
empty symmetric irreflexive RelStr for
a,
b,
c,
d being
Element of
G for
Z being
Subset of
G st
Z = {a,b,c,d} &
a,
b,
c,
d are_mutually_different &
[a,b] in the
InternalRel of
G &
[b,c] in the
InternalRel of
G &
[c,d] in the
InternalRel of
G & not
[a,c] in the
InternalRel of
G & not
[a,d] in the
InternalRel of
G & not
[b,d] in the
InternalRel of
G holds
subrelstr Z embeds Necklace 4
theorem Th40: :: NECKLA_3:40
theorem :: NECKLA_3:41