:: GLIB_002 semantic presentation

registration

let c₁ be finite set ;
cluster bool a₁ -> finite ;
coherence by FINSET_1:24;

end;

theorem Th1: :: GLIB_002:1

for b₁ being finite set st 1 < card b₁ holds
ex b₂, b₃ being set st
( b₂ in b₁ & b₃ in b₁ & b₂ <> b₃ )

proof end;

definition

let c₁ be _Graph;
attr a₁ is connected means :Def1: :: GLIB_002:def 1
for b₁, b₂ being Vertex of a₁ ex b₃ being Walk of a₁ st b₃ is_Walk_from b₁,b₂;

end;

:: deftheorem Def1 defines connected GLIB_002:def 1 :

definition

let c₁ be _Graph;
attr a₁ is acyclic means :Def2: :: GLIB_002:def 2
for b₁ being Walk of a₁ holds not b₁ is Cycle-like;

end;

:: deftheorem Def2 defines acyclic GLIB_002:def 2 :

definition

let c₁ be _Graph;
attr a₁ is Tree-like means :Def3: :: GLIB_002:def 3
( a₁ is acyclic & a₁ is connected );

end;

:: deftheorem Def3 defines Tree-like GLIB_002:def 3 :

registration

cluster trivial -> connected GraphStruct ;
coherence

proof end;

end;

registration

cluster loopless trivial -> Tree-like GraphStruct ;
coherence

proof end;

end;

registration

cluster acyclic -> simple GraphStruct ;
coherence

proof end;

end;

registration

cluster Tree-like -> simple connected acyclic GraphStruct ;
coherence by Def3;

end;

registration

cluster connected acyclic -> simple connected acyclic Tree-like GraphStruct ;
coherence by Def3;

end;

registration

let c₁ be _Graph;
let c₂ be Vertex of c₁;
cluster -> Tree-like inducedSubgraph of a₁,{a₂}, {} ;
coherence ;

end;

definition

let c₁ be _Graph;
let c₂ be set ;
pred c₁ is_DTree_rooted_at c₂ means :Def4: :: GLIB_002:def 4
( a₁ is Tree-like & ( for b₁ being Vertex of a₁ ex b₂ being DWalk of a₁ st b₂ is_Walk_from a₂,b₁ ) );

end;

:: deftheorem Def4 defines is_DTree_rooted_at GLIB_002:def 4 :

registration

cluster finite trivial simple connected acyclic Tree-like GraphStruct ;
existence

proof end;

cluster finite non trivial simple connected acyclic Tree-like GraphStruct ;
existence

proof end;

end;

registration

let c₁ be _Graph;
cluster finite trivial simple connected acyclic Tree-like Subgraph of a₁;
existence

proof end;

end;

registration

let c₁ be acyclic _Graph;
cluster -> acyclic Subgraph of a₁;
coherence

proof end;

end;

definition

let c₁ be _Graph;
let c₂ be Vertex of c₁;
func c₁ .reachableFrom c₂ -> non empty Subset of (the_Vertices_of a₁) means :Def5: :: GLIB_002:def 5
for b₁ being set holds
( b₁ in a₃ iff ex b₂ being Walk of a₁ st b₂ is_Walk_from a₂,b₁ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines .reachableFrom GLIB_002:def 5 :

definition

let c₁ be _Graph;
let c₂ be Vertex of c₁;
func c₁ .reachableDFrom c₂ -> non empty Subset of (the_Vertices_of a₁) means :Def6: :: GLIB_002:def 6
for b₁ being set holds
( b₁ in a₃ iff ex b₂ being DWalk of a₁ st b₂ is_Walk_from a₂,b₁ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines .reachableDFrom GLIB_002:def 6 :

Lemma8: for b₁ being _Graph
for b₂ being Vertex of b₁ holds b₂ in b₁ .reachableFrom b₂

proof end;

Lemma9: for b₁ being _Graph
for b₂ being Vertex of b₁
for b₃, b₄, b₅ being set st b₄ in b₁ .reachableFrom b₂ & b₃ Joins b₄,b₅,b₁ holds
b₅ in b₁ .reachableFrom b₂

proof end;

Lemma10: for b₁ being _Graph
for b₂, b₃ being Vertex of b₁ st b₂ in b₁ .reachableFrom b₃ holds
b₁ .reachableFrom b₂ = b₁ .reachableFrom b₃

proof end;

Lemma11: for b₁ being _Graph
for b₂ being Walk of b₁
for b₃ being Vertex of b₁ st b₃ in b₂ .vertices() holds
b₂ .vertices() c= b₁ .reachableFrom b₃

proof end;

definition

let c₁ be _Graph;
let c₂ be Subgraph of c₁;
attr a₂ is Component-like means :Def7: :: GLIB_002:def 7
( a₂ is connected & ( for b₁ being connected Subgraph of a₁ holds not a₂ c< b₁ ) );

end;

:: deftheorem Def7 defines Component-like GLIB_002:def 7 :

registration

let c₁ be _Graph;
cluster Component-like -> connected Subgraph of a₁;
coherence by Def7;

end;

registration

let c₁ be _Graph;
let c₂ be Vertex of c₁;
cluster -> connected Component-like inducedSubgraph of a₁,a₁ .reachableFrom a₂,a₁ .edgesBetween (a₁ .reachableFrom a₂);
coherence

proof end;

end;

registration

let c₁ be _Graph;
cluster connected Component-like Subgraph of a₁;
existence

proof end;

end;

definition

let c₁ be _Graph;
mode Component of a₁ is Component-like Subgraph of a₁;

end;

definition

let c₁ be _Graph;
func c₁ .componentSet() -> non empty Subset-Family of (the_Vertices_of a₁) means :Def8: :: GLIB_002:def 8
for b₁ being set holds
( b₁ in a₂ iff ex b₂ being Vertex of a₁ st b₁ = a₁ .reachableFrom b₂ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines .componentSet() GLIB_002:def 8 :

registration

let c₁ be _Graph;
let c₂ be Element of c₁ .componentSet() ;
cluster -> connected Component-like inducedSubgraph of a₁,a₂,a₁ .edgesBetween a₂;
coherence

proof end;

end;

definition

let c₁ be _Graph;
func c₁ .numComponents() -> Cardinal equals :: GLIB_002:def 9
Card (a₁ .componentSet() );
coherence ;

end;

:: deftheorem Def9 defines .numComponents() GLIB_002:def 9 :

definition

let c₁ be finite _Graph;
redefine func .numComponents() as c₁ .numComponents() -> non empty Nat;
coherence

proof end;

end;

definition

let c₁ be _Graph;
let c₂ be Vertex of c₁;
attr a₂ is cut-vertex means :Def10: :: GLIB_002:def 10
for b₁ being removeVertex of a₁,a₂ holds a₁ .numComponents() <` b₁ .numComponents() ;

end;

:: deftheorem Def10 defines cut-vertex GLIB_002:def 10 :

definition

let c₁ be finite _Graph;
let c₂ be Vertex of c₁;
redefine attr a₂ is cut-vertex means :Def11: :: GLIB_002:def 11
for b₁ being removeVertex of a₁,a₂ holds a₁ .numComponents() < b₁ .numComponents() ;
compatibility

proof end;

end;

:: deftheorem Def11 defines cut-vertex GLIB_002:def 11 :

Lemma16: for b₁ being non trivial connected _Graph
for b₂ being Vertex of b₁
for b₃ being removeVertex of b₁,b₂ st b₂ is endvertex holds
b₃ is connected

proof end;

Lemma17: for b₁ being _Graph st ex b₂ being Vertex of b₁ st
for b₃ being Vertex of b₁ ex b₄ being Walk of b₁ st b₄ is_Walk_from b₂,b₃ holds
b₁ is connected

proof end;

Lemma18: for b₁ being _Graph st ex b₂ being Vertex of b₁ st b₁ .reachableFrom b₂ = the_Vertices_of b₁ holds
b₁ is connected

proof end;

Lemma19: for b₁ being _Graph st b₁ is connected holds
for b₂ being Vertex of b₁ holds b₁ .reachableFrom b₂ = the_Vertices_of b₁

proof end;

Lemma20: for b₁, b₂ being _Graph
for b₃ being Vertex of b₁
for b₄ being Vertex of b₂ st b₁ == b₂ & b₃ = b₄ holds
b₁ .reachableFrom b₃ = b₂ .reachableFrom b₄

proof end;

Lemma21: for b₁ being _Graph
for b₂ being connected Subgraph of b₁ st b₂ is spanning holds
b₁ is connected

proof end;

Lemma22: for b₁ being _Graph holds
( b₁ is connected iff b₁ .componentSet() = {(the_Vertices_of b₁)} )

proof end;

Lemma23: for b₁, b₂ being _Graph st b₁ == b₂ holds
b₁ .componentSet() = b₂ .componentSet()

proof end;

Lemma24: for b₁ being _Graph
for b₂ being set st b₂ in b₁ .componentSet() holds
b₂ is non empty Subset of (the_Vertices_of b₁)

proof end;

Lemma25: for b₁ being _Graph
for b₂ being Component of b₁ holds the_Edges_of b₂ = b₁ .edgesBetween (the_Vertices_of b₂)

proof end;

Lemma26: for b₁ being _Graph
for b₂, b₃ being Component of b₁ holds
( the_Vertices_of b₂ = the_Vertices_of b₃ iff b₂ == b₃ )

proof end;

Lemma27: for b₁ being _Graph
for b₂ being Component of b₁
for b₃ being Vertex of b₁ holds
( b₃ in the_Vertices_of b₂ iff the_Vertices_of b₂ = b₁ .reachableFrom b₃ )

proof end;

Lemma28: for b₁ being _Graph
for b₂, b₃ being Component of b₁
for b₄ being set st b₄ in the_Vertices_of b₂ & b₄ in the_Vertices_of b₃ holds
b₂ == b₃

proof end;

Lemma29: for b₁ being _Graph holds
( b₁ is connected iff b₁ .numComponents() = 1 )

proof end;

Lemma30: for b₁, b₂ being _Graph st b₁ == b₂ holds
b₁ .numComponents() = b₂ .numComponents()
by Lemma23;

Lemma31: for b₁ being connected _Graph
for b₂ being Vertex of b₁ holds
( not b₂ is cut-vertex iff for b₃ being removeVertex of b₁,b₂ holds b₃ .numComponents() <=` b₁ .numComponents() )

proof end;

Lemma32: for b₁ being connected _Graph
for b₂ being Vertex of b₁
for b₃ being removeVertex of b₁,b₂ st not b₂ is cut-vertex holds
b₃ is connected

proof end;

Lemma33: for b₁ being finite non trivial connected _Graph ex b₂, b₃ being Vertex of b₁ st
( b₂ <> b₃ & not b₂ is cut-vertex & not b₃ is cut-vertex )

proof end;

registration

let c₁ be finite non trivial connected _Graph;
cluster non cut-vertex Element of the_Vertices_of a₁;
existence

proof end;

end;

Lemma34: for b₁ being acyclic _Graph
for b₂ being Path of b₁
for b₃ being set st not b₃ in b₂ .edges() & b₃ in (b₂ .last() ) .edgesInOut() holds
b₂ .addEdge b₃ is Path-like

proof end;

Lemma35: for b₁ being finite non trivial acyclic _Graph st the_Edges_of b₁ <> {} holds
ex b₂, b₃ being Vertex of b₁ st
( b₂ <> b₃ & b₂ is endvertex & b₃ is endvertex & b₃ in b₁ .reachableFrom b₂ )

proof end;

Lemma36: for b₁ being finite non trivial Tree-like _Graph ex b₂, b₃ being Vertex of b₁ st
( b₂ <> b₃ & b₂ is endvertex & b₃ is endvertex )

proof end;

registration

let c₁ be finite non trivial Tree-like _Graph;
cluster endvertex Element of the_Vertices_of a₁;
existence

proof end;

end;

registration

let c₁ be finite non trivial Tree-like _Graph;
let c₂ be endvertex Vertex of c₁;
cluster -> acyclic Tree-like inducedSubgraph of a₁,K132((the_Vertices_of a₁),{a₂}),a₁ .edgesBetween K132((the_Vertices_of a₁),{a₂});
coherence

proof end;

end;

definition

let c₁ be GraphSeq;
attr a₁ is connected means :Def12: :: GLIB_002:def 12
for b₁ being Nat holds a₁ .-> b₁ is connected;
attr a₁ is acyclic means :Def13: :: GLIB_002:def 13
for b₁ being Nat holds a₁ .-> b₁ is acyclic;
attr a₁ is Tree-like means :Def14: :: GLIB_002:def 14
for b₁ being Nat holds a₁ .-> b₁ is Tree-like;

end;

:: deftheorem Def12 defines connected GLIB_002:def 12 :

:: deftheorem Def13 defines acyclic GLIB_002:def 13 :

:: deftheorem Def14 defines Tree-like GLIB_002:def 14 :

registration

cluster trivial -> connected ManySortedSet of NAT ;
coherence

proof end;

cluster loopless trivial -> Tree-like ManySortedSet of NAT ;
coherence

proof end;

cluster acyclic -> simple ManySortedSet of NAT ;
coherence

proof end;

cluster Tree-like -> connected acyclic ManySortedSet of NAT ;
coherence

proof end;

cluster connected acyclic -> Tree-like ManySortedSet of NAT ;
coherence

proof end;

end;

registration

cluster halting finite simple connected acyclic Tree-like ManySortedSet of NAT ;
existence

proof end;

end;

registration

let c₁ be connected GraphSeq;
let c₂ be Nat;
cluster a₁ .-> a₂ -> connected ;
coherence by Def12;

end;

registration

let c₁ be acyclic GraphSeq;
let c₂ be Nat;
cluster a₁ .-> a₂ -> acyclic ;
coherence by Def13;

end;

registration

let c₁ be Tree-like GraphSeq;
let c₂ be Nat;
cluster a₁ .-> a₂ -> connected acyclic Tree-like ;
coherence ;

end;

theorem Th2: :: GLIB_002:2

for b₁ being non trivial connected _Graph
for b₂ being Vertex of b₁ holds not b₂ is isolated

proof end;

theorem Th3: :: GLIB_002:3

for b₁ being non trivial _Graph
for b₂ being Vertex of b₁
for b₃ being removeVertex of b₁,b₂ st b₃ is connected & ex b₄ being set st
( b₄ in b₂ .edgesInOut() & not b₄ Joins b₂,b₂,b₁ ) holds
b₁ is connected

proof end;

theorem Th4: :: GLIB_002:4

for b₁ being non trivial connected _Graph
for b₂ being Vertex of b₁
for b₃ being removeVertex of b₁,b₂ st b₂ is endvertex holds
b₃ is connected by Lemma16;

theorem Th5: :: GLIB_002:5

for b₁ being connected _Graph
for b₂ being Walk of b₁
for b₃ being set
for b₄ being removeEdge of b₁,b₃ st b₂ is Cycle-like & b₃ in b₂ .edges() holds
b₄ is connected

proof end;

theorem Th6: :: GLIB_002:6

for b₁ being _Graph st ex b₂ being Vertex of b₁ st
for b₃ being Vertex of b₁ ex b₄ being Walk of b₁ st b₄ is_Walk_from b₂,b₃ holds
b₁ is connected by Lemma17;

theorem Th7: :: GLIB_002:7

for b₁ being trivial _Graph holds b₁ is connected ;

theorem Th8: :: GLIB_002:8

for b₁, b₂ being _Graph st b₁ == b₂ & b₁ is connected holds
b₂ is connected

proof end;

theorem Th9: :: GLIB_002:9

for b₁ being _Graph
for b₂ being Vertex of b₁ holds b₂ in b₁ .reachableFrom b₂ by Lemma8;

theorem Th10: :: GLIB_002:10

for b₁ being _Graph
for b₂, b₃, b₄ being set
for b₅ being Vertex of b₁ st b₂ in b₁ .reachableFrom b₅ & b₃ Joins b₂,b₄,b₁ holds
b₄ in b₁ .reachableFrom b₅ by Lemma9;

theorem Th11: :: GLIB_002:11

for b₁ being _Graph
for b₂ being Vertex of b₁ holds b₁ .edgesBetween (b₁ .reachableFrom b₂) = b₁ .edgesInOut (b₁ .reachableFrom b₂)

proof end;

theorem Th12: :: GLIB_002:12

for b₁ being _Graph
for b₂, b₃ being Vertex of b₁ st b₂ in b₁ .reachableFrom b₃ holds
b₁ .reachableFrom b₂ = b₁ .reachableFrom b₃ by Lemma10;

theorem Th13: :: GLIB_002:13

for b₁ being _Graph
for b₂ being Vertex of b₁
for b₃ being Walk of b₁ st b₂ in b₃ .vertices() holds
b₃ .vertices() c= b₁ .reachableFrom b₂ by Lemma11;

theorem Th14: :: GLIB_002:14

for b₁ being _Graph
for b₂ being Subgraph of b₁
for b₃ being Vertex of b₁
for b₄ being Vertex of b₂ st b₃ = b₄ holds
b₂ .reachableFrom b₄ c= b₁ .reachableFrom b₃

proof end;

theorem Th15: :: GLIB_002:15

for b₁ being _Graph st ex b₂ being Vertex of b₁ st b₁ .reachableFrom b₂ = the_Vertices_of b₁ holds
b₁ is connected by Lemma18;

theorem Th16: :: GLIB_002:16

for b₁ being _Graph st b₁ is connected holds
for b₂ being Vertex of b₁ holds b₁ .reachableFrom b₂ = the_Vertices_of b₁ by Lemma19;

theorem Th17: :: GLIB_002:17

for b₁, b₂ being _Graph
for b₃ being Vertex of b₁
for b₄ being Vertex of b₂ st b₁ == b₂ & b₃ = b₄ holds
b₁ .reachableFrom b₃ = b₂ .reachableFrom b₄ by Lemma20;

theorem Th18: :: GLIB_002:18

for b₁ being _Graph
for b₂ being Vertex of b₁ holds b₂ in b₁ .reachableDFrom b₂

proof end;

theorem Th19: :: GLIB_002:19

for b₁ being _Graph
for b₂, b₃, b₄ being set
for b₅ being Vertex of b₁ st b₂ in b₁ .reachableDFrom b₅ & b₃ DJoins b₂,b₄,b₁ holds
b₄ in b₁ .reachableDFrom b₅

proof end;

theorem Th20: :: GLIB_002:20

for b₁ being _Graph
for b₂ being Vertex of b₁ holds b₁ .reachableDFrom b₂ c= b₁ .reachableFrom b₂

proof end;

theorem Th21: :: GLIB_002:21

for b₁ being _Graph
for b₂ being Subgraph of b₁
for b₃ being Vertex of b₁
for b₄ being Vertex of b₂ st b₃ = b₄ holds
b₂ .reachableDFrom b₄ c= b₁ .reachableDFrom b₃

proof end;

theorem Th22: :: GLIB_002:22

for b₁, b₂ being _Graph
for b₃ being Vertex of b₁
for b₄ being Vertex of b₂ st b₁ == b₂ & b₃ = b₄ holds
b₁ .reachableDFrom b₃ = b₂ .reachableDFrom b₄

proof end;

theorem Th23: :: GLIB_002:23

for b₁ being _Graph
for b₂ being connected Subgraph of b₁ st b₂ is spanning holds
b₁ is connected by Lemma21;

theorem Th24: :: GLIB_002:24

for b₁ being _Graph holds union (b₁ .componentSet() ) = the_Vertices_of b₁

proof end;

theorem Th25: :: GLIB_002:25

for b₁ being _Graph holds
( b₁ is connected iff b₁ .componentSet() = {(the_Vertices_of b₁)} ) by Lemma22;

theorem Th26: :: GLIB_002:26

for b₁, b₂ being _Graph st b₁ == b₂ holds
b₁ .componentSet() = b₂ .componentSet() by Lemma23;

theorem Th27: :: GLIB_002:27

for b₁ being _Graph
for b₂ being set st b₂ in b₁ .componentSet() holds
b₂ is non empty Subset of (the_Vertices_of b₁) by Lemma24;

theorem Th28: :: GLIB_002:28

for b₁ being _Graph holds
( b₁ is connected iff b₁ .numComponents() = 1 ) by Lemma29;

theorem Th29: :: GLIB_002:29

for b₁, b₂ being _Graph st b₁ == b₂ holds
b₁ .numComponents() = b₂ .numComponents() by Lemma30;

theorem Th30: :: GLIB_002:30

for b₁ being _Graph holds
( b₁ is Component of b₁ iff b₁ is connected )

proof end;

theorem Th31: :: GLIB_002:31

for b₁ being _Graph
for b₂ being Component of b₁ holds the_Edges_of b₂ = b₁ .edgesBetween (the_Vertices_of b₂) by Lemma25;

theorem Th32: :: GLIB_002:32

for b₁ being _Graph
for b₂, b₃ being Component of b₁ holds
( the_Vertices_of b₂ = the_Vertices_of b₃ iff b₂ == b₃ ) by Lemma26;

theorem Th33: :: GLIB_002:33

for b₁ being _Graph
for b₂ being Component of b₁
for b₃ being Vertex of b₁ holds
( b₃ in the_Vertices_of b₂ iff the_Vertices_of b₂ = b₁ .reachableFrom b₃ ) by Lemma27;

theorem Th34: :: GLIB_002:34

for b₁ being _Graph
for b₂, b₃ being Component of b₁
for b₄ being set st b₄ in the_Vertices_of b₂ & b₄ in the_Vertices_of b₃ holds
b₂ == b₃ by Lemma28;

theorem Th35: :: GLIB_002:35

for b₁ being connected _Graph
for b₂ being Vertex of b₁ holds
( not b₂ is cut-vertex iff for b₃ being removeVertex of b₁,b₂ holds b₃ .numComponents() <=` b₁ .numComponents() ) by Lemma31;

theorem Th36: :: GLIB_002:36

for b₁ being connected _Graph
for b₂ being Vertex of b₁
for b₃ being removeVertex of b₁,b₂ st not b₂ is cut-vertex holds
b₃ is connected by Lemma32;

theorem Th37: :: GLIB_002:37

for b₁ being finite non trivial connected _Graph ex b₂, b₃ being Vertex of b₁ st
( b₂ <> b₃ & not b₂ is cut-vertex & not b₃ is cut-vertex ) by Lemma33;

theorem Th38: :: GLIB_002:38

for b₁ being _Graph
for b₂ being Vertex of b₁ st b₂ is cut-vertex holds
not b₁ is trivial

proof end;

theorem Th39: :: GLIB_002:39

for b₁, b₂ being _Graph
for b₃ being Vertex of b₁
for b₄ being Vertex of b₂ st b₁ == b₂ & b₃ = b₄ & b₃ is cut-vertex holds
b₄ is cut-vertex

proof end;

theorem Th40: :: GLIB_002:40

for b₁ being finite connected _Graph holds b₁ .order() <= (b₁ .size() ) + 1

proof end;

theorem Th41: :: GLIB_002:41

for b₁ being acyclic _Graph holds b₁ is simple ;

theorem Th42: :: GLIB_002:42

for b₁ being acyclic _Graph
for b₂ being Path of b₁
for b₃ being set st not b₃ in b₂ .edges() & b₃ in (b₂ .last() ) .edgesInOut() holds
b₂ .addEdge b₃ is Path-like by Lemma34;

theorem Th43: :: GLIB_002:43

for b₁ being finite non trivial acyclic _Graph st the_Edges_of b₁ <> {} holds
ex b₂, b₃ being Vertex of b₁ st
( b₂ <> b₃ & b₂ is endvertex & b₃ is endvertex & b₃ in b₁ .reachableFrom b₂ ) by Lemma35;

theorem Th44: :: GLIB_002:44

for b₁, b₂ being _Graph st b₁ == b₂ & b₁ is acyclic holds
b₂ is acyclic

proof end;

theorem Th45: :: GLIB_002:45

for b₁ being finite non trivial Tree-like _Graph ex b₂, b₃ being Vertex of b₁ st
( b₂ <> b₃ & b₂ is endvertex & b₃ is endvertex ) by Lemma36;

theorem Th46: :: GLIB_002:46

for b₁ being finite _Graph holds
( b₁ is Tree-like iff ( b₁ is acyclic & b₁ .order() = (b₁ .size() ) + 1 ) )

proof end;

theorem Th47: :: GLIB_002:47

for b₁ being finite _Graph holds
( b₁ is Tree-like iff ( b₁ is connected & b₁ .order() = (b₁ .size() ) + 1 ) )

proof end;

theorem Th48: :: GLIB_002:48

for b₁, b₂ being _Graph st b₁ == b₂ & b₁ is Tree-like holds
b₂ is Tree-like

proof end;

theorem Th49: :: GLIB_002:49

for b₁ being _Graph
for b₂ being set st b₁ is_DTree_rooted_at b₂ holds
b₂ is Vertex of b₁

proof end;

theorem Th50: :: GLIB_002:50

for b₁, b₂ being _Graph
for b₃ being set st b₁ == b₂ & b₁ is_DTree_rooted_at b₃ holds
b₂ is_DTree_rooted_at b₃

proof end;