:: by Sebastian Koch

::

:: Received May 19, 2020

:: Copyright (c) 2020-2021 Association of Mizar Users

definition

let X be set ;

end;
attr X is Graph-membered means :Def1: :: GLIB_014:def 1

for x being object st x in X holds

x is _Graph;

for x being object st x in X holds

x is _Graph;

:: deftheorem Def1 defines Graph-membered GLIB_014:def 1 :

for X being set holds

( X is Graph-membered iff for x being object st x in X holds

x is _Graph );

for X being set holds

( X is Graph-membered iff for x being object st x in X holds

x is _Graph );

registration

let G1 be _Graph;

coherence

{G1} is Graph-membered by TARSKI:def 1;

let G2 be _Graph;

coherence

{G1,G2} is Graph-membered

end;
coherence

{G1} is Graph-membered by TARSKI:def 1;

let G2 be _Graph;

coherence

{G1,G2} is Graph-membered

proof end;

registration

existence

ex b_{1} being set st

( b_{1} is empty & b_{1} is Graph-membered )

ex b_{1} being set st

( b_{1} is trivial & b_{1} is finite & not b_{1} is empty & b_{1} is Graph-membered )

end;
ex b

( b

proof end;

existence ex b

( b

proof end;

registration

let X be Graph-membered set ;

coherence

for b_{1} being Subset of X holds b_{1} is Graph-membered
by Def1;

end;
coherence

for b

:: the usual set operations preserve graph membership

registration

let X be Graph-membered set ;

let Y be set ;

coherence

X /\ Y is Graph-membered

X \ Y is Graph-membered ;

end;
let Y be set ;

coherence

X /\ Y is Graph-membered

proof end;

coherence X \ Y is Graph-membered ;

registration

let X, Y be Graph-membered set ;

coherence

X \/ Y is Graph-membered

X \+\ Y is Graph-membered ;

end;
coherence

X \/ Y is Graph-membered

proof end;

coherence X \+\ Y is Graph-membered ;

theorem :: GLIB_014:1

for X being set st ( for Y being object st Y in X holds

Y is Graph-membered set ) holds

union X is Graph-membered

Y is Graph-membered set ) holds

union X is Graph-membered

proof end;

registration

let X be non empty Graph-membered set ;

coherence

for b_{1} being Element of X holds

( b_{1} is Function-like & b_{1} is Relation-like )
by Def1;

end;
coherence

for b

( b

registration

let X be non empty Graph-membered set ;

coherence

for b_{1} being Element of X holds

( b_{1} is NAT -defined & b_{1} is finite )
by Def1;

end;
coherence

for b

( b

registration

let X be non empty Graph-membered set ;

coherence

for b_{1} being Element of X holds b_{1} is [Graph-like]
by Def1;

end;
coherence

for b

:: several graphs attributes for sets of graphs

:: ("finite" and "trivial" are deliberately omitted,

:: so that the set attributes are not overridden)

:: ("finite" and "trivial" are deliberately omitted,

:: so that the set attributes are not overridden)

definition

let S be Graph-membered set ;

end;
attr S is loopless means :Def3: :: GLIB_014:def 3

for G being _Graph st G in S holds

G is loopless ;

for G being _Graph st G in S holds

G is loopless ;

attr S is non-multi means :Def4: :: GLIB_014:def 4

for G being _Graph st G in S holds

G is non-multi ;

for G being _Graph st G in S holds

G is non-multi ;

attr S is non-Dmulti means :Def5: :: GLIB_014:def 5

for G being _Graph st G in S holds

G is non-Dmulti ;

for G being _Graph st G in S holds

G is non-Dmulti ;

attr S is connected means :Def9: :: GLIB_014:def 9

for G being _Graph st G in S holds

G is connected ;

for G being _Graph st G in S holds

G is connected ;

attr S is chordal means :Def11: :: GLIB_014:def 11

for G being _Graph st G in S holds

G is chordal ;

for G being _Graph st G in S holds

G is chordal ;

:: deftheorem Def2 defines plain GLIB_014:def 2 :

for S being Graph-membered set holds

( S is plain iff for G being _Graph st G in S holds

G is plain );

for S being Graph-membered set holds

( S is plain iff for G being _Graph st G in S holds

G is plain );

:: deftheorem Def3 defines loopless GLIB_014:def 3 :

for S being Graph-membered set holds

( S is loopless iff for G being _Graph st G in S holds

G is loopless );

for S being Graph-membered set holds

( S is loopless iff for G being _Graph st G in S holds

G is loopless );

:: deftheorem Def4 defines non-multi GLIB_014:def 4 :

for S being Graph-membered set holds

( S is non-multi iff for G being _Graph st G in S holds

G is non-multi );

for S being Graph-membered set holds

( S is non-multi iff for G being _Graph st G in S holds

G is non-multi );

:: deftheorem Def5 defines non-Dmulti GLIB_014:def 5 :

for S being Graph-membered set holds

( S is non-Dmulti iff for G being _Graph st G in S holds

G is non-Dmulti );

for S being Graph-membered set holds

( S is non-Dmulti iff for G being _Graph st G in S holds

G is non-Dmulti );

:: deftheorem defines simple GLIB_014:def 6 :

for S being Graph-membered set holds

( S is simple iff for G being _Graph st G in S holds

G is simple );

for S being Graph-membered set holds

( S is simple iff for G being _Graph st G in S holds

G is simple );

:: deftheorem defines Dsimple GLIB_014:def 7 :

for S being Graph-membered set holds

( S is Dsimple iff for G being _Graph st G in S holds

G is Dsimple );

for S being Graph-membered set holds

( S is Dsimple iff for G being _Graph st G in S holds

G is Dsimple );

:: deftheorem Def8 defines acyclic GLIB_014:def 8 :

for S being Graph-membered set holds

( S is acyclic iff for G being _Graph st G in S holds

G is acyclic );

for S being Graph-membered set holds

( S is acyclic iff for G being _Graph st G in S holds

G is acyclic );

:: deftheorem Def9 defines connected GLIB_014:def 9 :

for S being Graph-membered set holds

( S is connected iff for G being _Graph st G in S holds

G is connected );

for S being Graph-membered set holds

( S is connected iff for G being _Graph st G in S holds

G is connected );

:: deftheorem defines Tree-like GLIB_014:def 10 :

for S being Graph-membered set holds

( S is Tree-like iff for G being _Graph st G in S holds

G is Tree-like );

for S being Graph-membered set holds

( S is Tree-like iff for G being _Graph st G in S holds

G is Tree-like );

:: deftheorem Def11 defines chordal GLIB_014:def 11 :

for S being Graph-membered set holds

( S is chordal iff for G being _Graph st G in S holds

G is chordal );

for S being Graph-membered set holds

( S is chordal iff for G being _Graph st G in S holds

G is chordal );

:: deftheorem Def12 defines edgeless GLIB_014:def 12 :

for S being Graph-membered set holds

( S is edgeless iff for G being _Graph st G in S holds

G is edgeless );

for S being Graph-membered set holds

( S is edgeless iff for G being _Graph st G in S holds

G is edgeless );

:: deftheorem Def13 defines loopfull GLIB_014:def 13 :

for S being Graph-membered set holds

( S is loopfull iff for G being _Graph st G in S holds

G is loopfull );

for S being Graph-membered set holds

( S is loopfull iff for G being _Graph st G in S holds

G is loopfull );

:: negative clustering are omitted, because

:: negative attributes (e.g. "non-loopless") are not defined yet

:: negative attributes (e.g. "non-loopless") are not defined yet

registration

for b_{1} being Graph-membered set st b_{1} is empty holds

( b_{1} is plain & b_{1} is loopless & b_{1} is non-multi & b_{1} is non-Dmulti & b_{1} is simple & b_{1} is Dsimple & b_{1} is acyclic & b_{1} is connected & b_{1} is Tree-like & b_{1} is chordal & b_{1} is edgeless & b_{1} is loopfull )
;

coherence

for b_{1} being Graph-membered set st b_{1} is non-multi holds

b_{1} is non-Dmulti

for b_{1} being Graph-membered set st b_{1} is loopless & b_{1} is non-multi holds

b_{1} is simple

for b_{1} being Graph-membered set st b_{1} is loopless & b_{1} is non-Dmulti holds

b_{1} is Dsimple

for b_{1} being Graph-membered set st b_{1} is simple holds

( b_{1} is loopless & b_{1} is non-multi )

for b_{1} being Graph-membered set st b_{1} is Dsimple holds

( b_{1} is loopless & b_{1} is non-Dmulti )

for b_{1} being Graph-membered set st b_{1} is acyclic holds

b_{1} is simple

for b_{1} being Graph-membered set st b_{1} is acyclic & b_{1} is connected holds

b_{1} is Tree-like

for b_{1} being Graph-membered set st b_{1} is Tree-like holds

( b_{1} is acyclic & b_{1} is connected )
end;

cluster empty Graph-membered -> Graph-membered plain loopless non-multi non-Dmulti simple Dsimple acyclic connected Tree-like chordal edgeless loopfull for set ;

coherence for b

( b

coherence

for b

b

proof end;

coherence for b

b

proof end;

coherence for b

b

proof end;

coherence for b

( b

proof end;

coherence for b

( b

proof end;

coherence for b

b

proof end;

coherence for b

b

proof end;

coherence for b

( b

proof end;

registration

let G1 be plain _Graph;

coherence

{G1} is plain by TARSKI:def 1;

let G2 be plain _Graph;

coherence

{G1,G2} is plain

end;
coherence

{G1} is plain by TARSKI:def 1;

let G2 be plain _Graph;

coherence

{G1,G2} is plain

proof end;

registration

let G1 be loopless _Graph;

coherence

{G1} is loopless by TARSKI:def 1;

let G2 be loopless _Graph;

coherence

{G1,G2} is loopless

end;
coherence

{G1} is loopless by TARSKI:def 1;

let G2 be loopless _Graph;

coherence

{G1,G2} is loopless

proof end;

registration

let G1 be non-multi _Graph;

coherence

{G1} is non-multi by TARSKI:def 1;

let G2 be non-multi _Graph;

coherence

{G1,G2} is non-multi

end;
coherence

{G1} is non-multi by TARSKI:def 1;

let G2 be non-multi _Graph;

coherence

{G1,G2} is non-multi

proof end;

registration

let G1 be non-Dmulti _Graph;

coherence

{G1} is non-Dmulti by TARSKI:def 1;

let G2 be non-Dmulti _Graph;

coherence

{G1,G2} is non-Dmulti

end;
coherence

{G1} is non-Dmulti by TARSKI:def 1;

let G2 be non-Dmulti _Graph;

coherence

{G1,G2} is non-Dmulti

proof end;

registration

let G1 be simple _Graph;

coherence

{G1} is simple ;

let G2 be simple _Graph;

coherence

{G1,G2} is simple ;

end;
coherence

{G1} is simple ;

let G2 be simple _Graph;

coherence

{G1,G2} is simple ;

registration

let G1 be Dsimple _Graph;

coherence

{G1} is Dsimple ;

let G2 be Dsimple _Graph;

coherence

{G1,G2} is Dsimple ;

end;
coherence

{G1} is Dsimple ;

let G2 be Dsimple _Graph;

coherence

{G1,G2} is Dsimple ;

registration

let G1 be acyclic _Graph;

coherence

{G1} is acyclic by TARSKI:def 1;

let G2 be acyclic _Graph;

coherence

{G1,G2} is acyclic

end;
coherence

{G1} is acyclic by TARSKI:def 1;

let G2 be acyclic _Graph;

coherence

{G1,G2} is acyclic

proof end;

registration

let G1 be connected _Graph;

coherence

{G1} is connected by TARSKI:def 1;

let G2 be connected _Graph;

coherence

{G1,G2} is connected

end;
coherence

{G1} is connected by TARSKI:def 1;

let G2 be connected _Graph;

coherence

{G1,G2} is connected

proof end;

registration

let G1 be Tree-like _Graph;

coherence

{G1} is Tree-like ;

let G2 be Tree-like _Graph;

coherence

{G1,G2} is Tree-like ;

end;
coherence

{G1} is Tree-like ;

let G2 be Tree-like _Graph;

coherence

{G1,G2} is Tree-like ;

registration

let G1 be chordal _Graph;

coherence

{G1} is chordal by TARSKI:def 1;

let G2 be chordal _Graph;

coherence

{G1,G2} is chordal

end;
coherence

{G1} is chordal by TARSKI:def 1;

let G2 be chordal _Graph;

coherence

{G1,G2} is chordal

proof end;

registration

let G1 be edgeless _Graph;

coherence

{G1} is edgeless by TARSKI:def 1;

let G2 be edgeless _Graph;

coherence

{G1,G2} is edgeless

end;
coherence

{G1} is edgeless by TARSKI:def 1;

let G2 be edgeless _Graph;

coherence

{G1,G2} is edgeless

proof end;

registration

let G1 be loopfull _Graph;

coherence

{G1} is loopfull by TARSKI:def 1;

let G2 be loopfull _Graph;

coherence

{G1,G2} is loopfull

end;
coherence

{G1} is loopfull by TARSKI:def 1;

let G2 be loopfull _Graph;

coherence

{G1,G2} is loopfull

proof end;

::registration

::let G1 be vertex-finite _Graph;

::cluster {G1} -> vertex-finite;

::coherence;

::let G2 be vertex-finite _Graph;

::cluster {G1, G2} -> vertex-finite;

::coherence;

::end;

::

::registration

::let G1 be edge-finite _Graph;

::cluster {G1} -> edge-finite;

::coherence;

::let G2 be edge-finite _Graph;

::cluster {G1, G2} -> edge-finite;

::coherence;

::end;

:: attributes given through graph yielding functions

::let G1 be vertex-finite _Graph;

::cluster {G1} -> vertex-finite;

::coherence;

::let G2 be vertex-finite _Graph;

::cluster {G1, G2} -> vertex-finite;

::coherence;

::end;

::

::registration

::let G1 be edge-finite _Graph;

::cluster {G1} -> edge-finite;

::coherence;

::let G2 be edge-finite _Graph;

::cluster {G1, G2} -> edge-finite;

::coherence;

::end;

:: attributes given through graph yielding functions

theorem Th3: :: GLIB_014:3

for F being Graph-yielding Function holds

( ( F is plain implies rng F is plain ) & ( rng F is plain implies F is plain ) & ( F is loopless implies rng F is loopless ) & ( rng F is loopless implies F is loopless ) & ( F is non-multi implies rng F is non-multi ) & ( rng F is non-multi implies F is non-multi ) & ( F is non-Dmulti implies rng F is non-Dmulti ) & ( rng F is non-Dmulti implies F is non-Dmulti ) & ( F is acyclic implies rng F is acyclic ) & ( rng F is acyclic implies F is acyclic ) & ( F is connected implies rng F is connected ) & ( rng F is connected implies F is connected ) & ( F is chordal implies rng F is chordal ) & ( rng F is chordal implies F is chordal ) & ( F is edgeless implies rng F is edgeless ) & ( rng F is edgeless implies F is edgeless ) & ( F is loopfull implies rng F is loopfull ) & ( rng F is loopfull implies F is loopfull ) )

( ( F is plain implies rng F is plain ) & ( rng F is plain implies F is plain ) & ( F is loopless implies rng F is loopless ) & ( rng F is loopless implies F is loopless ) & ( F is non-multi implies rng F is non-multi ) & ( rng F is non-multi implies F is non-multi ) & ( F is non-Dmulti implies rng F is non-Dmulti ) & ( rng F is non-Dmulti implies F is non-Dmulti ) & ( F is acyclic implies rng F is acyclic ) & ( rng F is acyclic implies F is acyclic ) & ( F is connected implies rng F is connected ) & ( rng F is connected implies F is connected ) & ( F is chordal implies rng F is chordal ) & ( rng F is chordal implies F is chordal ) & ( F is edgeless implies rng F is edgeless ) & ( rng F is edgeless implies F is edgeless ) & ( F is loopfull implies rng F is loopfull ) & ( rng F is loopfull implies F is loopfull ) )

proof end;

theorem Th4: :: GLIB_014:4

for F being Graph-yielding Function holds

( ( F is simple implies rng F is simple ) & ( rng F is simple implies F is simple ) & ( F is Dsimple implies rng F is Dsimple ) & ( rng F is Dsimple implies F is Dsimple ) & ( F is Tree-like implies rng F is Tree-like ) & ( rng F is Tree-like implies F is Tree-like ) )

( ( F is simple implies rng F is simple ) & ( rng F is simple implies F is simple ) & ( F is Dsimple implies rng F is Dsimple ) & ( rng F is Dsimple implies F is Dsimple ) & ( F is Tree-like implies rng F is Tree-like ) & ( rng F is Tree-like implies F is Tree-like ) )

proof end;

registration
end;

registration
end;

registration
end;

registration
end;

::registration

::let F be vertex-finite Graph-yielding Function;

::cluster rng F -> vertex-finite;

::coherence

::proof

::let G be _Graph;

::assume G in rng F;

::then consider x being object such that

::A1: x in dom F & F.x = G by FUNCT_1:def 3;

::consider G0 being _Graph such that

::A2: F.x = G0 & G0 is vertex-finite by A1, GLIB_012:def 2;

::thus G is vertex-finite by A1, A2;

::end;

::end;

::

::registration

::let F be edge-finite Graph-yielding Function;

::cluster rng F -> edge-finite;

::coherence

::proof

::let G be _Graph;

::assume G in rng F;

::then consider x being object such that

::A1: x in dom F & F.x = G by FUNCT_1:def 3;

::consider G0 being _Graph such that

::A2: F.x = G0 & G0 is edge-finite by A1, GLIB_012:def 2;

::thus G is edge-finite by A1, A2;

::end;

::end;

:: attributes of graph subsets

::let F be vertex-finite Graph-yielding Function;

::cluster rng F -> vertex-finite;

::coherence

::proof

::let G be _Graph;

::assume G in rng F;

::then consider x being object such that

::A1: x in dom F & F.x = G by FUNCT_1:def 3;

::consider G0 being _Graph such that

::A2: F.x = G0 & G0 is vertex-finite by A1, GLIB_012:def 2;

::thus G is vertex-finite by A1, A2;

::end;

::end;

::

::registration

::let F be edge-finite Graph-yielding Function;

::cluster rng F -> edge-finite;

::coherence

::proof

::let G be _Graph;

::assume G in rng F;

::then consider x being object such that

::A1: x in dom F & F.x = G by FUNCT_1:def 3;

::consider G0 being _Graph such that

::A2: F.x = G0 & G0 is edge-finite by A1, GLIB_012:def 2;

::thus G is edge-finite by A1, A2;

::end;

::end;

:: attributes of graph subsets

registration

let X be Graph-membered plain set ;

coherence

for b_{1} being Subset of X holds b_{1} is plain
by Def2;

end;
coherence

for b

registration

let X be Graph-membered loopless set ;

coherence

for b_{1} being Subset of X holds b_{1} is loopless
by Def3;

end;
coherence

for b

registration

let X be Graph-membered non-multi set ;

coherence

for b_{1} being Subset of X holds b_{1} is non-multi
by Def4;

end;
coherence

for b

registration

let X be Graph-membered non-Dmulti set ;

coherence

for b_{1} being Subset of X holds b_{1} is non-Dmulti
by Def5;

end;
coherence

for b

registration
end;

registration

let X be Graph-membered Dsimple set ;

coherence

for b_{1} being Subset of X holds b_{1} is Dsimple
;

end;
coherence

for b

registration

let X be Graph-membered acyclic set ;

coherence

for b_{1} being Subset of X holds b_{1} is acyclic
by Def8;

end;
coherence

for b

registration

let X be Graph-membered connected set ;

coherence

for b_{1} being Subset of X holds b_{1} is connected
by Def9;

end;
coherence

for b

registration

let X be Graph-membered Tree-like set ;

coherence

for b_{1} being Subset of X holds b_{1} is Tree-like
;

end;
coherence

for b

registration

let X be Graph-membered chordal set ;

coherence

for b_{1} being Subset of X holds b_{1} is chordal
by Def11;

end;
coherence

for b

registration

let X be Graph-membered edgeless set ;

coherence

for b_{1} being Subset of X holds b_{1} is edgeless
by Def12;

end;
coherence

for b

registration

let X be Graph-membered loopfull set ;

coherence

for b_{1} being Subset of X holds b_{1} is loopfull
by Def13;

end;
coherence

for b

::registration

::let X be vertex-finite Graph-membered set;

::cluster -> vertex-finite for Subset of X;

::coherence by Def16;

::end;

::

::registration

::let X be edge-finite Graph-membered set;

::cluster -> edge-finite for Subset of X;

::coherence by Def16;

::end;

:: attributes of graph sets and set operations

::let X be vertex-finite Graph-membered set;

::cluster -> vertex-finite for Subset of X;

::coherence by Def16;

::end;

::

::registration

::let X be edge-finite Graph-membered set;

::cluster -> edge-finite for Subset of X;

::coherence by Def16;

::end;

:: attributes of graph sets and set operations

registration

let X be Graph-membered plain set ;

let Y be set ;

coherence

X /\ Y is plain

X \ Y is plain ;

end;
let Y be set ;

coherence

X /\ Y is plain

proof end;

coherence X \ Y is plain ;

registration

let X, Y be Graph-membered plain set ;

coherence

X \/ Y is plain

X \+\ Y is plain ;

end;
coherence

X \/ Y is plain

proof end;

coherence X \+\ Y is plain ;

registration

let X be Graph-membered loopless set ;

let Y be set ;

coherence

X /\ Y is loopless

X \ Y is loopless ;

end;
let Y be set ;

coherence

X /\ Y is loopless

proof end;

coherence X \ Y is loopless ;

registration

let X, Y be Graph-membered loopless set ;

coherence

X \/ Y is loopless

X \+\ Y is loopless ;

end;
coherence

X \/ Y is loopless

proof end;

coherence X \+\ Y is loopless ;

registration

let X be Graph-membered non-multi set ;

let Y be set ;

coherence

X /\ Y is non-multi

X \ Y is non-multi ;

end;
let Y be set ;

coherence

X /\ Y is non-multi

proof end;

coherence X \ Y is non-multi ;

registration

let X, Y be Graph-membered non-multi set ;

coherence

X \/ Y is non-multi

X \+\ Y is non-multi ;

end;
coherence

X \/ Y is non-multi

proof end;

coherence X \+\ Y is non-multi ;

registration

let X be Graph-membered non-Dmulti set ;

let Y be set ;

coherence

X /\ Y is non-Dmulti

X \ Y is non-Dmulti ;

end;
let Y be set ;

coherence

X /\ Y is non-Dmulti

proof end;

coherence X \ Y is non-Dmulti ;

registration

let X, Y be Graph-membered non-Dmulti set ;

coherence

X \/ Y is non-Dmulti

X \+\ Y is non-Dmulti ;

end;
coherence

X \/ Y is non-Dmulti

proof end;

coherence X \+\ Y is non-Dmulti ;

registration

let X be Graph-membered simple set ;

let Y be set ;

coherence

X /\ Y is simple ;

coherence

X \ Y is simple ;

end;
let Y be set ;

coherence

X /\ Y is simple ;

coherence

X \ Y is simple ;

registration
end;

registration

let X be Graph-membered Dsimple set ;

let Y be set ;

coherence

X /\ Y is Dsimple ;

coherence

X \ Y is Dsimple ;

end;
let Y be set ;

coherence

X /\ Y is Dsimple ;

coherence

X \ Y is Dsimple ;

registration

let X, Y be Graph-membered Dsimple set ;

coherence

X \/ Y is Dsimple ;

coherence

X \+\ Y is Dsimple ;

end;
coherence

X \/ Y is Dsimple ;

coherence

X \+\ Y is Dsimple ;

registration

let X be Graph-membered acyclic set ;

let Y be set ;

coherence

X /\ Y is acyclic

X \ Y is acyclic ;

end;
let Y be set ;

coherence

X /\ Y is acyclic

proof end;

coherence X \ Y is acyclic ;

registration

let X, Y be Graph-membered acyclic set ;

coherence

X \/ Y is acyclic

X \+\ Y is acyclic ;

end;
coherence

X \/ Y is acyclic

proof end;

coherence X \+\ Y is acyclic ;

registration

let X be Graph-membered connected set ;

let Y be set ;

coherence

X /\ Y is connected

X \ Y is connected ;

end;
let Y be set ;

coherence

X /\ Y is connected

proof end;

coherence X \ Y is connected ;

registration

let X, Y be Graph-membered connected set ;

coherence

X \/ Y is connected

X \+\ Y is connected ;

end;
coherence

X \/ Y is connected

proof end;

coherence X \+\ Y is connected ;

registration

let X be Graph-membered Tree-like set ;

let Y be set ;

coherence

X /\ Y is Tree-like ;

coherence

X \ Y is Tree-like ;

end;
let Y be set ;

coherence

X /\ Y is Tree-like ;

coherence

X \ Y is Tree-like ;

registration

let X, Y be Graph-membered Tree-like set ;

coherence

X \/ Y is Tree-like ;

coherence

X \+\ Y is Tree-like ;

end;
coherence

X \/ Y is Tree-like ;

coherence

X \+\ Y is Tree-like ;

registration

let X be Graph-membered chordal set ;

let Y be set ;

coherence

X /\ Y is chordal

X \ Y is chordal ;

end;
let Y be set ;

coherence

X /\ Y is chordal

proof end;

coherence X \ Y is chordal ;

registration

let X, Y be Graph-membered chordal set ;

coherence

X \/ Y is chordal

X \+\ Y is chordal ;

end;
coherence

X \/ Y is chordal

proof end;

coherence X \+\ Y is chordal ;

registration

let X be Graph-membered edgeless set ;

let Y be set ;

coherence

X /\ Y is edgeless

X \ Y is edgeless ;

end;
let Y be set ;

coherence

X /\ Y is edgeless

proof end;

coherence X \ Y is edgeless ;

registration

let X, Y be Graph-membered edgeless set ;

coherence

X \/ Y is edgeless

X \+\ Y is edgeless ;

end;
coherence

X \/ Y is edgeless

proof end;

coherence X \+\ Y is edgeless ;

registration

let X be Graph-membered loopfull set ;

let Y be set ;

coherence

X /\ Y is loopfull

X \ Y is loopfull ;

end;
let Y be set ;

coherence

X /\ Y is loopfull

proof end;

coherence X \ Y is loopfull ;

registration

let X, Y be Graph-membered loopfull set ;

coherence

X \/ Y is loopfull

X \+\ Y is loopfull ;

end;
coherence

X \/ Y is loopfull

proof end;

coherence X \+\ Y is loopfull ;

::registration

::let X be vertex-finite Graph-membered set, Y be set;

::cluster X /\ Y -> vertex-finite;

::coherence

::proof

::X /\ Y c= X by XBOOLE_1:17;

::hence thesis;

::end;

::cluster X \ Y -> vertex-finite;

::coherence;

::end;

::

::registration

::let X, Y be vertex-finite Graph-membered set;

::cluster X \/ Y -> vertex-finite;

::coherence

::proof

::let x be _Graph;

::assume x in X \/ Y;

::then per cases by XBOOLE_0:def 3;

::suppose x in X;

::hence thesis by Def16;

::end;

::suppose x in Y;

::hence thesis by Def16;

::end;

::end;

::cluster X \+\ Y -> vertex-finite;

::coherence

::proof

::X \+\ Y = (X \ Y) \/ (Y \ X) by XBOOLE_0:def 6;

::hence thesis;

::end;

::end;

::

::registration

::let X be edge-finite Graph-membered set, Y be set;

::cluster X /\ Y -> edge-finite;

::coherence

::proof

::X /\ Y c= X by XBOOLE_1:17;

::hence thesis;

::end;

::cluster X \ Y -> edge-finite;

::coherence;

::end;

::

::registration

::let X, Y be edge-finite Graph-membered set;

::cluster X \/ Y -> edge-finite;

::coherence

::proof

::let x be _Graph;

::assume x in X \/ Y;

::then per cases by XBOOLE_0:def 3;

::suppose x in X;

::hence thesis by Def16;

::end;

::suppose x in Y;

::hence thesis by Def16;

::end;

::end;

::cluster X \+\ Y -> edge-finite;

::coherence

::proof

::X \+\ Y = (X \ Y) \/ (Y \ X) by XBOOLE_0:def 6;

::hence thesis;

::end;

::end;

:: existence clusters for all attributes

::let X be vertex-finite Graph-membered set, Y be set;

::cluster X /\ Y -> vertex-finite;

::coherence

::proof

::X /\ Y c= X by XBOOLE_1:17;

::hence thesis;

::end;

::cluster X \ Y -> vertex-finite;

::coherence;

::end;

::

::registration

::let X, Y be vertex-finite Graph-membered set;

::cluster X \/ Y -> vertex-finite;

::coherence

::proof

::let x be _Graph;

::assume x in X \/ Y;

::then per cases by XBOOLE_0:def 3;

::suppose x in X;

::hence thesis by Def16;

::end;

::suppose x in Y;

::hence thesis by Def16;

::end;

::end;

::cluster X \+\ Y -> vertex-finite;

::coherence

::proof

::X \+\ Y = (X \ Y) \/ (Y \ X) by XBOOLE_0:def 6;

::hence thesis;

::end;

::end;

::

::registration

::let X be edge-finite Graph-membered set, Y be set;

::cluster X /\ Y -> edge-finite;

::coherence

::proof

::X /\ Y c= X by XBOOLE_1:17;

::hence thesis;

::end;

::cluster X \ Y -> edge-finite;

::coherence;

::end;

::

::registration

::let X, Y be edge-finite Graph-membered set;

::cluster X \/ Y -> edge-finite;

::coherence

::proof

::let x be _Graph;

::assume x in X \/ Y;

::then per cases by XBOOLE_0:def 3;

::suppose x in X;

::hence thesis by Def16;

::end;

::suppose x in Y;

::hence thesis by Def16;

::end;

::end;

::cluster X \+\ Y -> edge-finite;

::coherence

::proof

::X \+\ Y = (X \ Y) \/ (Y \ X) by XBOOLE_0:def 6;

::hence thesis;

::end;

::end;

:: existence clusters for all attributes

registration

ex b_{1} being Graph-membered set st

( b_{1} is empty & b_{1} is plain & b_{1} is loopless & b_{1} is non-multi & b_{1} is non-Dmulti & b_{1} is simple & b_{1} is Dsimple & b_{1} is acyclic & b_{1} is connected & b_{1} is Tree-like & b_{1} is chordal & b_{1} is edgeless & b_{1} is loopfull )

ex b_{1} being Graph-membered set st

( not b_{1} is empty & b_{1} is Tree-like & b_{1} is acyclic & b_{1} is connected & b_{1} is simple & b_{1} is Dsimple & b_{1} is loopless & b_{1} is non-multi & b_{1} is non-Dmulti )

ex b_{1} being Graph-membered set st

( not b_{1} is empty & b_{1} is edgeless & b_{1} is chordal )

ex b_{1} being Graph-membered set st

( not b_{1} is empty & b_{1} is loopfull )

ex b_{1} being Graph-membered set st

( not b_{1} is empty & b_{1} is plain )
end;

cluster empty Graph-membered plain loopless non-multi non-Dmulti simple Dsimple acyclic connected Tree-like chordal edgeless loopfull for set ;

existence ex b

( b

proof end;

cluster non empty Graph-membered loopless non-multi non-Dmulti simple Dsimple acyclic connected Tree-like for set ;

existence ex b

( not b

proof end;

existence ex b

( not b

proof end;

existence ex b

( not b

proof end;

existence ex b

( not b

proof end;

registration

let S be non empty Graph-membered plain set ;

coherence

for b_{1} being Element of S holds b_{1} is plain
by Def2;

end;
coherence

for b

registration

let S be non empty Graph-membered loopless set ;

coherence

for b_{1} being Element of S holds b_{1} is loopless
by Def3;

end;
coherence

for b

registration

let S be non empty Graph-membered non-multi set ;

coherence

for b_{1} being Element of S holds b_{1} is non-multi
by Def4;

end;
coherence

for b

registration

let S be non empty Graph-membered non-Dmulti set ;

coherence

for b_{1} being Element of S holds b_{1} is non-Dmulti
by Def5;

end;
coherence

for b

registration

let S be non empty Graph-membered simple set ;

coherence

for b_{1} being Element of S holds b_{1} is simple
;

end;
coherence

for b

registration

let S be non empty Graph-membered Dsimple set ;

coherence

for b_{1} being Element of S holds b_{1} is Dsimple
;

end;
coherence

for b

registration

let S be non empty Graph-membered acyclic set ;

coherence

for b_{1} being Element of S holds b_{1} is acyclic
by Def8;

end;
coherence

for b

registration

let S be non empty Graph-membered connected set ;

coherence

for b_{1} being Element of S holds b_{1} is connected
by Def9;

end;
coherence

for b

registration

let S be non empty Graph-membered Tree-like set ;

coherence

for b_{1} being Element of S holds b_{1} is Tree-like
;

end;
coherence

for b

registration

let S be non empty Graph-membered chordal set ;

coherence

for b_{1} being Element of S holds b_{1} is chordal
by Def11;

end;
coherence

for b

registration

let S be non empty Graph-membered edgeless set ;

coherence

for b_{1} being Element of S holds b_{1} is edgeless
by Def12;

end;
coherence

for b

registration

let S be non empty Graph-membered loopfull set ;

coherence

for b_{1} being Element of S holds b_{1} is loopfull
by Def13;

end;
coherence

for b

::registration

::let S be non empty vertex-finite Graph-membered set;

::cluster -> vertex-finite for Element of S;

::coherence by Def16;

::end;

::

::registration

::let S be non empty edge-finite Graph-membered set;

::cluster -> edge-finite for Element of S;

::coherence by Def16;

::end;

:: getting vertices/edges/sources/targets from the Graph-membered set

::let S be non empty vertex-finite Graph-membered set;

::cluster -> vertex-finite for Element of S;

::coherence by Def16;

::end;

::

::registration

::let S be non empty edge-finite Graph-membered set;

::cluster -> edge-finite for Element of S;

::coherence by Def16;

::end;

:: getting vertices/edges/sources/targets from the Graph-membered set

definition

let S be Graph-membered set ;

ex b_{1} being set st

for V being object holds

( V in b_{1} iff ex G being _Graph st

( G in S & V = the_Vertices_of G ) )

for b_{1}, b_{2} being set st ( for V being object holds

( V in b_{1} iff ex G being _Graph st

( G in S & V = the_Vertices_of G ) ) ) & ( for V being object holds

( V in b_{2} iff ex G being _Graph st

( G in S & V = the_Vertices_of G ) ) ) holds

b_{1} = b_{2}

ex b_{1} being set st

for E being object holds

( E in b_{1} iff ex G being _Graph st

( G in S & E = the_Edges_of G ) )

for b_{1}, b_{2} being set st ( for E being object holds

( E in b_{1} iff ex G being _Graph st

( G in S & E = the_Edges_of G ) ) ) & ( for E being object holds

( E in b_{2} iff ex G being _Graph st

( G in S & E = the_Edges_of G ) ) ) holds

b_{1} = b_{2}

ex b_{1} being set st

for s being object holds

( s in b_{1} iff ex G being _Graph st

( G in S & s = the_Source_of G ) )

for b_{1}, b_{2} being set st ( for s being object holds

( s in b_{1} iff ex G being _Graph st

( G in S & s = the_Source_of G ) ) ) & ( for s being object holds

( s in b_{2} iff ex G being _Graph st

( G in S & s = the_Source_of G ) ) ) holds

b_{1} = b_{2}

ex b_{1} being set st

for t being object holds

( t in b_{1} iff ex G being _Graph st

( G in S & t = the_Target_of G ) )

for b_{1}, b_{2} being set st ( for t being object holds

( t in b_{1} iff ex G being _Graph st

( G in S & t = the_Target_of G ) ) ) & ( for t being object holds

( t in b_{2} iff ex G being _Graph st

( G in S & t = the_Target_of G ) ) ) holds

b_{1} = b_{2}

end;
func the_Vertices_of S -> set means :Def14: :: GLIB_014:def 14

for V being object holds

( V in it iff ex G being _Graph st

( G in S & V = the_Vertices_of G ) );

existence for V being object holds

( V in it iff ex G being _Graph st

( G in S & V = the_Vertices_of G ) );

ex b

for V being object holds

( V in b

( G in S & V = the_Vertices_of G ) )

proof end;

uniqueness for b

( V in b

( G in S & V = the_Vertices_of G ) ) ) & ( for V being object holds

( V in b

( G in S & V = the_Vertices_of G ) ) ) holds

b

proof end;

func the_Edges_of S -> set means :Def15: :: GLIB_014:def 15

for E being object holds

( E in it iff ex G being _Graph st

( G in S & E = the_Edges_of G ) );

existence for E being object holds

( E in it iff ex G being _Graph st

( G in S & E = the_Edges_of G ) );

ex b

for E being object holds

( E in b

( G in S & E = the_Edges_of G ) )

proof end;

uniqueness for b

( E in b

( G in S & E = the_Edges_of G ) ) ) & ( for E being object holds

( E in b

( G in S & E = the_Edges_of G ) ) ) holds

b

proof end;

func the_Source_of S -> set means :Def16: :: GLIB_014:def 16

for s being object holds

( s in it iff ex G being _Graph st

( G in S & s = the_Source_of G ) );

existence for s being object holds

( s in it iff ex G being _Graph st

( G in S & s = the_Source_of G ) );

ex b

for s being object holds

( s in b

( G in S & s = the_Source_of G ) )

proof end;

uniqueness for b

( s in b

( G in S & s = the_Source_of G ) ) ) & ( for s being object holds

( s in b

( G in S & s = the_Source_of G ) ) ) holds

b

proof end;

func the_Target_of S -> set means :Def17: :: GLIB_014:def 17

for t being object holds

( t in it iff ex G being _Graph st

( G in S & t = the_Target_of G ) );

existence for t being object holds

( t in it iff ex G being _Graph st

( G in S & t = the_Target_of G ) );

ex b

for t being object holds

( t in b

( G in S & t = the_Target_of G ) )

proof end;

uniqueness for b

( t in b

( G in S & t = the_Target_of G ) ) ) & ( for t being object holds

( t in b

( G in S & t = the_Target_of G ) ) ) holds

b

proof end;

:: deftheorem Def14 defines the_Vertices_of GLIB_014:def 14 :

for S being Graph-membered set

for b_{2} being set holds

( b_{2} = the_Vertices_of S iff for V being object holds

( V in b_{2} iff ex G being _Graph st

( G in S & V = the_Vertices_of G ) ) );

for S being Graph-membered set

for b

( b

( V in b

( G in S & V = the_Vertices_of G ) ) );

:: deftheorem Def15 defines the_Edges_of GLIB_014:def 15 :

for S being Graph-membered set

for b_{2} being set holds

( b_{2} = the_Edges_of S iff for E being object holds

( E in b_{2} iff ex G being _Graph st

( G in S & E = the_Edges_of G ) ) );

for S being Graph-membered set

for b

( b

( E in b

( G in S & E = the_Edges_of G ) ) );

:: deftheorem Def16 defines the_Source_of GLIB_014:def 16 :

for S being Graph-membered set

for b_{2} being set holds

( b_{2} = the_Source_of S iff for s being object holds

( s in b_{2} iff ex G being _Graph st

( G in S & s = the_Source_of G ) ) );

for S being Graph-membered set

for b

( b

( s in b

( G in S & s = the_Source_of G ) ) );

:: deftheorem Def17 defines the_Target_of GLIB_014:def 17 :

for S being Graph-membered set

for b_{2} being set holds

( b_{2} = the_Target_of S iff for t being object holds

( t in b_{2} iff ex G being _Graph st

( G in S & t = the_Target_of G ) ) );

for S being Graph-membered set

for b

( b

( t in b

( G in S & t = the_Target_of G ) ) );

definition

let S be non empty Graph-membered set ;

for b_{1} being set holds

( b_{1} = the_Vertices_of S iff b_{1} = { (the_Vertices_of G) where G is Element of S : verum } )

for b_{1} being set holds

( b_{1} = the_Edges_of S iff b_{1} = { (the_Edges_of G) where G is Element of S : verum } )

for b_{1} being set holds

( b_{1} = the_Source_of S iff b_{1} = { (the_Source_of G) where G is Element of S : verum } )

for b_{1} being set holds

( b_{1} = the_Target_of S iff b_{1} = { (the_Target_of G) where G is Element of S : verum } )

end;
redefine func the_Vertices_of S equals :: GLIB_014:def 18

{ (the_Vertices_of G) where G is Element of S : verum } ;

compatibility { (the_Vertices_of G) where G is Element of S : verum } ;

for b

( b

proof end;

redefine func the_Edges_of S equals :: GLIB_014:def 19

{ (the_Edges_of G) where G is Element of S : verum } ;

compatibility { (the_Edges_of G) where G is Element of S : verum } ;

for b

( b

proof end;

redefine func the_Source_of S equals :: GLIB_014:def 20

{ (the_Source_of G) where G is Element of S : verum } ;

compatibility { (the_Source_of G) where G is Element of S : verum } ;

for b

( b

proof end;

redefine func the_Target_of S equals :: GLIB_014:def 21

{ (the_Target_of G) where G is Element of S : verum } ;

compatibility { (the_Target_of G) where G is Element of S : verum } ;

for b

( b

proof end;

:: deftheorem defines the_Vertices_of GLIB_014:def 18 :

for S being non empty Graph-membered set holds the_Vertices_of S = { (the_Vertices_of G) where G is Element of S : verum } ;

for S being non empty Graph-membered set holds the_Vertices_of S = { (the_Vertices_of G) where G is Element of S : verum } ;

:: deftheorem defines the_Edges_of GLIB_014:def 19 :

for S being non empty Graph-membered set holds the_Edges_of S = { (the_Edges_of G) where G is Element of S : verum } ;

for S being non empty Graph-membered set holds the_Edges_of S = { (the_Edges_of G) where G is Element of S : verum } ;

:: deftheorem defines the_Source_of GLIB_014:def 20 :

for S being non empty Graph-membered set holds the_Source_of S = { (the_Source_of G) where G is Element of S : verum } ;

for S being non empty Graph-membered set holds the_Source_of S = { (the_Source_of G) where G is Element of S : verum } ;

:: deftheorem defines the_Target_of GLIB_014:def 21 :

for S being non empty Graph-membered set holds the_Target_of S = { (the_Target_of G) where G is Element of S : verum } ;

for S being non empty Graph-membered set holds the_Target_of S = { (the_Target_of G) where G is Element of S : verum } ;

registration
end;

registration

let S be Graph-membered set ;

coherence

the_Source_of S is functional

the_Target_of S is functional

end;
coherence

the_Source_of S is functional

proof end;

coherence the_Target_of S is functional

proof end;

registration

let S be empty Graph-membered set ;

coherence

the_Vertices_of S is empty

the_Edges_of S is empty

the_Source_of S is empty

the_Target_of S is empty

end;
coherence

the_Vertices_of S is empty

proof end;

coherence the_Edges_of S is empty

proof end;

coherence the_Source_of S is empty

proof end;

coherence the_Target_of S is empty

proof end;

registration

let S be non empty Graph-membered set ;

coherence

not the_Vertices_of S is empty

not the_Edges_of S is empty

not the_Source_of S is empty

not the_Target_of S is empty

end;
coherence

not the_Vertices_of S is empty

proof end;

coherence not the_Edges_of S is empty

proof end;

coherence not the_Source_of S is empty

proof end;

coherence not the_Target_of S is empty

proof end;

registration

let S be trivial Graph-membered set ;

coherence

the_Vertices_of S is trivial

the_Edges_of S is trivial

the_Source_of S is trivial

the_Target_of S is trivial

end;
coherence

the_Vertices_of S is trivial

proof end;

coherence the_Edges_of S is trivial

proof end;

coherence the_Source_of S is trivial

proof end;

coherence the_Target_of S is trivial

proof end;

theorem Th5: :: GLIB_014:5

for G being _Graph holds

( the_Vertices_of {G} = {(the_Vertices_of G)} & the_Edges_of {G} = {(the_Edges_of G)} & the_Source_of {G} = {(the_Source_of G)} & the_Target_of {G} = {(the_Target_of G)} )

( the_Vertices_of {G} = {(the_Vertices_of G)} & the_Edges_of {G} = {(the_Edges_of G)} & the_Source_of {G} = {(the_Source_of G)} & the_Target_of {G} = {(the_Target_of G)} )

proof end;

theorem Th6: :: GLIB_014:6

for G, H being _Graph holds

( the_Vertices_of {G,H} = {(the_Vertices_of G),(the_Vertices_of H)} & the_Edges_of {G,H} = {(the_Edges_of G),(the_Edges_of H)} & the_Source_of {G,H} = {(the_Source_of G),(the_Source_of H)} & the_Target_of {G,H} = {(the_Target_of G),(the_Target_of H)} )

( the_Vertices_of {G,H} = {(the_Vertices_of G),(the_Vertices_of H)} & the_Edges_of {G,H} = {(the_Edges_of G),(the_Edges_of H)} & the_Source_of {G,H} = {(the_Source_of G),(the_Source_of H)} & the_Target_of {G,H} = {(the_Target_of G),(the_Target_of H)} )

proof end;

theorem Th7: :: GLIB_014:7

for S being Graph-membered set holds

( card (the_Vertices_of S) c= card S & card (the_Edges_of S) c= card S & card (the_Source_of S) c= card S & card (the_Target_of S) c= card S )

( card (the_Vertices_of S) c= card S & card (the_Edges_of S) c= card S & card (the_Source_of S) c= card S & card (the_Target_of S) c= card S )

proof end;

registration

let S be finite Graph-membered set ;

coherence

the_Vertices_of S is finite

the_Edges_of S is finite

the_Source_of S is finite

the_Target_of S is finite

end;
coherence

the_Vertices_of S is finite

proof end;

coherence the_Edges_of S is finite

proof end;

coherence the_Source_of S is finite

proof end;

coherence the_Target_of S is finite

proof end;

registration
end;

theorem Th8: :: GLIB_014:8

for S1, S2 being Graph-membered set holds

( the_Vertices_of (S1 \/ S2) = (the_Vertices_of S1) \/ (the_Vertices_of S2) & the_Edges_of (S1 \/ S2) = (the_Edges_of S1) \/ (the_Edges_of S2) & the_Source_of (S1 \/ S2) = (the_Source_of S1) \/ (the_Source_of S2) & the_Target_of (S1 \/ S2) = (the_Target_of S1) \/ (the_Target_of S2) )

( the_Vertices_of (S1 \/ S2) = (the_Vertices_of S1) \/ (the_Vertices_of S2) & the_Edges_of (S1 \/ S2) = (the_Edges_of S1) \/ (the_Edges_of S2) & the_Source_of (S1 \/ S2) = (the_Source_of S1) \/ (the_Source_of S2) & the_Target_of (S1 \/ S2) = (the_Target_of S1) \/ (the_Target_of S2) )

proof end;

:: no equality, for example take {G},{H} with G == H but G <> H

theorem :: GLIB_014:9

for S1, S2 being Graph-membered set holds

( the_Vertices_of (S1 /\ S2) c= (the_Vertices_of S1) /\ (the_Vertices_of S2) & the_Edges_of (S1 /\ S2) c= (the_Edges_of S1) /\ (the_Edges_of S2) & the_Source_of (S1 /\ S2) c= (the_Source_of S1) /\ (the_Source_of S2) & the_Target_of (S1 /\ S2) c= (the_Target_of S1) /\ (the_Target_of S2) )

( the_Vertices_of (S1 /\ S2) c= (the_Vertices_of S1) /\ (the_Vertices_of S2) & the_Edges_of (S1 /\ S2) c= (the_Edges_of S1) /\ (the_Edges_of S2) & the_Source_of (S1 /\ S2) c= (the_Source_of S1) /\ (the_Source_of S2) & the_Target_of (S1 /\ S2) c= (the_Target_of S1) /\ (the_Target_of S2) )

proof end;

theorem Th10: :: GLIB_014:10

for S1, S2 being Graph-membered set holds

( (the_Vertices_of S1) \ (the_Vertices_of S2) c= the_Vertices_of (S1 \ S2) & (the_Edges_of S1) \ (the_Edges_of S2) c= the_Edges_of (S1 \ S2) & (the_Source_of S1) \ (the_Source_of S2) c= the_Source_of (S1 \ S2) & (the_Target_of S1) \ (the_Target_of S2) c= the_Target_of (S1 \ S2) )

( (the_Vertices_of S1) \ (the_Vertices_of S2) c= the_Vertices_of (S1 \ S2) & (the_Edges_of S1) \ (the_Edges_of S2) c= the_Edges_of (S1 \ S2) & (the_Source_of S1) \ (the_Source_of S2) c= the_Source_of (S1 \ S2) & (the_Target_of S1) \ (the_Target_of S2) c= the_Target_of (S1 \ S2) )

proof end;

theorem :: GLIB_014:11

for S1, S2 being Graph-membered set holds

( (the_Vertices_of S1) \+\ (the_Vertices_of S2) c= the_Vertices_of (S1 \+\ S2) & (the_Edges_of S1) \+\ (the_Edges_of S2) c= the_Edges_of (S1 \+\ S2) & (the_Source_of S1) \+\ (the_Source_of S2) c= the_Source_of (S1 \+\ S2) & (the_Target_of S1) \+\ (the_Target_of S2) c= the_Target_of (S1 \+\ S2) )

( (the_Vertices_of S1) \+\ (the_Vertices_of S2) c= the_Vertices_of (S1 \+\ S2) & (the_Edges_of S1) \+\ (the_Edges_of S2) c= the_Edges_of (S1 \+\ S2) & (the_Source_of S1) \+\ (the_Source_of S2) c= the_Source_of (S1 \+\ S2) & (the_Target_of S1) \+\ (the_Target_of S2) c= the_Target_of (S1 \+\ S2) )

proof end;

definition

let G1, G2 be _Graph;

for G1 being _Graph holds

( the_Source_of G1 tolerates the_Source_of G1 & the_Target_of G1 tolerates the_Target_of G1 ) ;

symmetry

for G1, G2 being _Graph st the_Source_of G1 tolerates the_Source_of G2 & the_Target_of G1 tolerates the_Target_of G2 holds

( the_Source_of G2 tolerates the_Source_of G1 & the_Target_of G2 tolerates the_Target_of G1 ) ;

end;
pred G1 tolerates G2 means :: GLIB_014:def 22

( the_Source_of G1 tolerates the_Source_of G2 & the_Target_of G1 tolerates the_Target_of G2 );

reflexivity ( the_Source_of G1 tolerates the_Source_of G2 & the_Target_of G1 tolerates the_Target_of G2 );

for G1 being _Graph holds

( the_Source_of G1 tolerates the_Source_of G1 & the_Target_of G1 tolerates the_Target_of G1 ) ;

symmetry

for G1, G2 being _Graph st the_Source_of G1 tolerates the_Source_of G2 & the_Target_of G1 tolerates the_Target_of G2 holds

( the_Source_of G2 tolerates the_Source_of G1 & the_Target_of G2 tolerates the_Target_of G1 ) ;

:: deftheorem defines tolerates GLIB_014:def 22 :

for G1, G2 being _Graph holds

( G1 tolerates G2 iff ( the_Source_of G1 tolerates the_Source_of G2 & the_Target_of G1 tolerates the_Target_of G2 ) );

for G1, G2 being _Graph holds

( G1 tolerates G2 iff ( the_Source_of G1 tolerates the_Source_of G2 & the_Target_of G1 tolerates the_Target_of G2 ) );

theorem :: GLIB_014:13

for G1, G2 being _Graph st the_Source_of G1 c= the_Source_of G2 & the_Target_of G1 c= the_Target_of G2 holds

G1 tolerates G2 by PARTFUN1:54;

G1 tolerates G2 by PARTFUN1:54;

theorem Th17: :: GLIB_014:17

for G1, G2 being _Graph holds

( G1 tolerates G2 iff for e, v1, w1, v2, w2 being object st e DJoins v1,w1,G1 & e DJoins v2,w2,G2 holds

( v1 = v2 & w1 = w2 ) )

( G1 tolerates G2 iff for e, v1, w1, v2, w2 being object st e DJoins v1,w1,G1 & e DJoins v2,w2,G2 holds

( v1 = v2 & w1 = w2 ) )

proof end;

theorem :: GLIB_014:18

for G1 being _Graph

for E being Subset of (the_Edges_of G1)

for G2 being reverseEdgeDirections of G1,E holds

( G1 tolerates G2 iff E c= G1 .loops() )

for E being Subset of (the_Edges_of G1)

for G2 being reverseEdgeDirections of G1,E holds

( G1 tolerates G2 iff E c= G1 .loops() )

proof end;

definition

let S be Graph-membered set ;

end;
attr S is \/-tolerating means :Def23: :: GLIB_014:def 23

for G1, G2 being _Graph st G1 in S & G2 in S holds

G1 tolerates G2;

for G1, G2 being _Graph st G1 in S & G2 in S holds

G1 tolerates G2;

:: deftheorem Def23 defines \/-tolerating GLIB_014:def 23 :

for S being Graph-membered set holds

( S is \/-tolerating iff for G1, G2 being _Graph st G1 in S & G2 in S holds

G1 tolerates G2 );

for S being Graph-membered set holds

( S is \/-tolerating iff for G1, G2 being _Graph st G1 in S & G2 in S holds

G1 tolerates G2 );

definition

let S be non empty Graph-membered set ;

( S is \/-tolerating iff for G1, G2 being Element of S holds G1 tolerates G2 ) ;

end;
redefine attr S is \/-tolerating means :: GLIB_014:def 24

for G1, G2 being Element of S holds G1 tolerates G2;

compatibility for G1, G2 being Element of S holds G1 tolerates G2;

( S is \/-tolerating iff for G1, G2 being Element of S holds G1 tolerates G2 ) ;

:: deftheorem defines \/-tolerating GLIB_014:def 24 :

for S being non empty Graph-membered set holds

( S is \/-tolerating iff for G1, G2 being Element of S holds G1 tolerates G2 );

for S being non empty Graph-membered set holds

( S is \/-tolerating iff for G1, G2 being Element of S holds G1 tolerates G2 );

registration

coherence

for b_{1} being Graph-membered set st b_{1} is empty holds

b_{1} is \/-tolerating
;

let G be _Graph;

coherence

{G} is \/-tolerating

end;
for b

b

let G be _Graph;

coherence

{G} is \/-tolerating

proof end;

registration

existence

ex b_{1} being Graph-membered set st

( not b_{1} is empty & b_{1} is \/-tolerating )

end;
ex b

( not b

proof end;

registration

let S1 be Graph-membered \/-tolerating set ;

let S2 be set ;

coherence

S1 /\ S2 is \/-tolerating

S1 \ S2 is \/-tolerating by Def23;

end;
let S2 be set ;

coherence

S1 /\ S2 is \/-tolerating

proof end;

coherence S1 \ S2 is \/-tolerating by Def23;

theorem Th20: :: GLIB_014:20

for S1, S2 being Graph-membered set st S1 \/ S2 is \/-tolerating holds

( S1 is \/-tolerating & S2 is \/-tolerating )

( S1 is \/-tolerating & S2 is \/-tolerating )

proof end;

registration

let S be Graph-membered \/-tolerating set ;

coherence

the_Source_of S is compatible

the_Target_of S is compatible

end;
coherence

the_Source_of S is compatible

proof end;

coherence the_Target_of S is compatible

proof end;

registration

let S be Graph-membered \/-tolerating set ;

coherence

( union (the_Source_of S) is Function-like & union (the_Source_of S) is Relation-like ) ;

coherence

( union (the_Target_of S) is Function-like & union (the_Target_of S) is Relation-like ) ;

end;
coherence

( union (the_Source_of S) is Function-like & union (the_Source_of S) is Relation-like ) ;

coherence

( union (the_Target_of S) is Function-like & union (the_Target_of S) is Relation-like ) ;

registration

let S be Graph-membered \/-tolerating set ;

( union (the_Source_of S) is union (the_Edges_of S) -defined & union (the_Source_of S) is union (the_Vertices_of S) -valued )

( union (the_Target_of S) is union (the_Edges_of S) -defined & union (the_Target_of S) is union (the_Vertices_of S) -valued )

end;
cluster union (the_Source_of S) -> union (the_Edges_of S) -defined union (the_Vertices_of S) -valued ;

coherence ( union (the_Source_of S) is union (the_Edges_of S) -defined & union (the_Source_of S) is union (the_Vertices_of S) -valued )

proof end;

cluster union (the_Target_of S) -> union (the_Edges_of S) -defined union (the_Vertices_of S) -valued ;

coherence ( union (the_Target_of S) is union (the_Edges_of S) -defined & union (the_Target_of S) is union (the_Vertices_of S) -valued )

proof end;

registration

let S be Graph-membered \/-tolerating set ;

coherence

union (the_Source_of S) is total

union (the_Target_of S) is total

end;
coherence

union (the_Source_of S) is total

proof end;

coherence union (the_Target_of S) is total

proof end;

definition

let S be GraphUnionSet;

ex b_{1} being _Graph st

( the_Vertices_of b_{1} = union (the_Vertices_of S) & the_Edges_of b_{1} = union (the_Edges_of S) & the_Source_of b_{1} = union (the_Source_of S) & the_Target_of b_{1} = union (the_Target_of S) )

end;
mode GraphUnion of S -> _Graph means :Def25: :: GLIB_014:def 25

( the_Vertices_of it = union (the_Vertices_of S) & the_Edges_of it = union (the_Edges_of S) & the_Source_of it = union (the_Source_of S) & the_Target_of it = union (the_Target_of S) );

existence ( the_Vertices_of it = union (the_Vertices_of S) & the_Edges_of it = union (the_Edges_of S) & the_Source_of it = union (the_Source_of S) & the_Target_of it = union (the_Target_of S) );

ex b

( the_Vertices_of b

proof end;

:: deftheorem Def25 defines GraphUnion GLIB_014:def 25 :

for S being GraphUnionSet

for b_{2} being _Graph holds

( b_{2} is GraphUnion of S iff ( the_Vertices_of b_{2} = union (the_Vertices_of S) & the_Edges_of b_{2} = union (the_Edges_of S) & the_Source_of b_{2} = union (the_Source_of S) & the_Target_of b_{2} = union (the_Target_of S) ) );

for S being GraphUnionSet

for b

( b

:: not really needed

::definition

::let S be GraphUnionSet;

::func union S equals the plain GraphUnion of S;

::end;

:: not proven here (DOMS from VALUED_2)

:: theorem

:: for S being GraphUnionSet, G being GraphUnion of S

:: holds DOMS(the_Source_of S) = dom the_Source_of G &

:: DOMS(the_Target_of S) = dom the_Target_of G;

::definition

::let S be GraphUnionSet;

::func union S equals the plain GraphUnion of S;

::end;

:: not proven here (DOMS from VALUED_2)

:: theorem

:: for S being GraphUnionSet, G being GraphUnion of S

:: holds DOMS(the_Source_of S) = dom the_Source_of G &

:: DOMS(the_Target_of S) = dom the_Target_of G;

theorem Th21: :: GLIB_014:21

for S being GraphUnionSet

for G being GraphUnion of S

for H being Element of S holds H is Subgraph of G

for G being GraphUnion of S

for H being Element of S holds H is Subgraph of G

proof end;

theorem Th22: :: GLIB_014:22

for S being GraphUnionSet

for G being GraphUnion of S

for G9 being _Graph holds

( G9 is GraphUnion of S iff G == G9 )

for G being GraphUnion of S

for G9 being _Graph holds

( G9 is GraphUnion of S iff G == G9 )

proof end;

registration
end;

registration

existence

ex b_{1} being GraphUnionSet st b_{1} is loopless

ex b_{1} being GraphUnionSet st b_{1} is edgeless

ex b_{1} being GraphUnionSet st b_{1} is loopfull

end;
ex b

proof end;

existence ex b

proof end;

existence ex b

proof end;

theorem Th23: :: GLIB_014:23

for S being GraphUnionSet

for G being GraphUnion of S holds

( ( S is loopless implies G is loopless ) & ( G is loopless implies S is loopless ) & ( S is edgeless implies G is edgeless ) & ( G is edgeless implies S is edgeless ) & ( S is loopfull implies G is loopfull ) )

for G being GraphUnion of S holds

( ( S is loopless implies G is loopless ) & ( G is loopless implies S is loopless ) & ( S is edgeless implies G is edgeless ) & ( G is edgeless implies S is edgeless ) & ( S is loopfull implies G is loopfull ) )

proof end;

registration

let S be loopless GraphUnionSet;

coherence

for b_{1} being GraphUnion of S holds b_{1} is loopless
by Th23;

end;
coherence

for b

registration

let S be edgeless GraphUnionSet;

coherence

for b_{1} being GraphUnion of S holds b_{1} is edgeless
by Th23;

end;
coherence

for b

registration

let S be loopfull GraphUnionSet;

coherence

for b_{1} being GraphUnion of S holds b_{1} is loopfull
by Th23;

end;
coherence

for b

definition

let G1, G2 be _Graph;

( ( G1 tolerates G2 implies ex b_{1} being Supergraph of G1 ex S being GraphUnionSet st

( S = {G1,G2} & b_{1} is GraphUnion of S ) ) & ( not G1 tolerates G2 implies ex b_{1} being Supergraph of G1 st b_{1} == G1 ) )

for b_{1} being Supergraph of G1 holds verum
;

end;
mode GraphUnion of G1,G2 -> Supergraph of G1 means :Def26: :: GLIB_014:def 26

ex S being GraphUnionSet st

( S = {G1,G2} & it is GraphUnion of S ) if G1 tolerates G2

otherwise it == G1;

existence ex S being GraphUnionSet st

( S = {G1,G2} & it is GraphUnion of S ) if G1 tolerates G2

otherwise it == G1;

( ( G1 tolerates G2 implies ex b

( S = {G1,G2} & b

proof end;

consistency for b

:: deftheorem Def26 defines GraphUnion GLIB_014:def 26 :

for G1, G2 being _Graph

for b_{3} being Supergraph of G1 holds

( ( G1 tolerates G2 implies ( b_{3} is GraphUnion of G1,G2 iff ex S being GraphUnionSet st

( S = {G1,G2} & b_{3} is GraphUnion of S ) ) ) & ( not G1 tolerates G2 implies ( b_{3} is GraphUnion of G1,G2 iff b_{3} == G1 ) ) );

for G1, G2 being _Graph

for b

( ( G1 tolerates G2 implies ( b

( S = {G1,G2} & b

:: not really needed

::definition

::let G1, G2 be _Graph;

::func G1 \/ G2 equals the plain GraphUnion of G1, G2;

::end;

::definition

::let G1, G2 be _Graph;

::func G1 \/ G2 equals the plain GraphUnion of G1, G2;

::end;

theorem Th25: :: GLIB_014:25

for G1, G2, G being _Graph st G1 tolerates G2 holds

( G is GraphUnion of G1,G2 iff ( the_Vertices_of G = (the_Vertices_of G1) \/ (the_Vertices_of G2) & the_Edges_of G = (the_Edges_of G1) \/ (the_Edges_of G2) & the_Source_of G = (the_Source_of G1) +* (the_Source_of G2) & the_Target_of G = (the_Target_of G1) +* (the_Target_of G2) ) )

( G is GraphUnion of G1,G2 iff ( the_Vertices_of G = (the_Vertices_of G1) \/ (the_Vertices_of G2) & the_Edges_of G = (the_Edges_of G1) \/ (the_Edges_of G2) & the_Source_of G = (the_Source_of G1) +* (the_Source_of G2) & the_Target_of G = (the_Target_of G1) +* (the_Target_of G2) ) )

proof end;

theorem Th26: :: GLIB_014:26

for G1, G2 being _Graph

for G being GraphUnion of G1,G2 st G1 tolerates G2 holds

G is Supergraph of G2

for G being GraphUnion of G1,G2 st G1 tolerates G2 holds

G is Supergraph of G2

proof end;

theorem :: GLIB_014:27

for G1, G2 being _Graph

for G being GraphUnion of G1,G2 st G1 tolerates G2 holds

G is GraphUnion of G2,G1

for G being GraphUnion of G1,G2 st G1 tolerates G2 holds

G is GraphUnion of G2,G1

proof end;

theorem Th28: :: GLIB_014:28

for G1, G2, G9 being _Graph

for G being GraphUnion of G1,G2 holds

( G9 is GraphUnion of G1,G2 iff G == G9 )

for G being GraphUnion of G1,G2 holds

( G9 is GraphUnion of G1,G2 iff G == G9 )

proof end;

registration
end;

registration

let G1, G2 be loopless _Graph;

coherence

for b_{1} being GraphUnion of G1,G2 holds b_{1} is loopless

end;
coherence

for b

proof end;

registration

let G1, G2 be edgeless _Graph;

coherence

for b_{1} being GraphUnion of G1,G2 holds b_{1} is edgeless

end;
coherence

for b

proof end;

registration

let G1, G2 be loopfull _Graph;

coherence

for b_{1} being GraphUnion of G1,G2 holds b_{1} is loopfull

end;
coherence

for b

proof end;

theorem Th30: :: GLIB_014:30

for G1 being _Graph

for G2 being DLGraphComplement of G1

for G being GraphUnion of G1,G2

for v, w being Vertex of G ex e being object st e DJoins v,w,G

for G2 being DLGraphComplement of G1

for G being GraphUnion of G1,G2

for v, w being Vertex of G ex e being object st e DJoins v,w,G

proof end;

registration

let G1 be _Graph;

let G2 be DLGraphComplement of G1;

coherence

for b_{1} being GraphUnion of G1,G2 holds

( b_{1} is loopfull & b_{1} is complete )

end;
let G2 be DLGraphComplement of G1;

coherence

for b

( b

proof end;

theorem Th31: :: GLIB_014:31

for G1 being _Graph

for G2 being LGraphComplement of G1

for G being GraphUnion of G1,G2

for v, w being Vertex of G ex e being object st e Joins v,w,G

for G2 being LGraphComplement of G1

for G being GraphUnion of G1,G2

for v, w being Vertex of G ex e being object st e Joins v,w,G

proof end;

registration

let G1 be _Graph;

let G2 be LGraphComplement of G1;

coherence

for b_{1} being GraphUnion of G1,G2 holds

( b_{1} is loopfull & b_{1} is complete )

end;
let G2 be LGraphComplement of G1;

coherence

for b

( b

proof end;

theorem Th32: :: GLIB_014:32

for G1 being _Graph

for G2 being DGraphComplement of G1

for G being GraphUnion of G1,G2

for v, w being Vertex of G st v <> w holds

ex e being object st e DJoins v,w,G

for G2 being DGraphComplement of G1

for G being GraphUnion of G1,G2

for v, w being Vertex of G st v <> w holds

ex e being object st e DJoins v,w,G

proof end;

registration

let G1 be _Graph;

let G2 be DGraphComplement of G1;

coherence

for b_{1} being GraphUnion of G1,G2 holds b_{1} is complete

end;
let G2 be DGraphComplement of G1;

coherence

for b

proof end;

theorem Th33: :: GLIB_014:33

for G1 being _Graph

for G2 being GraphComplement of G1

for G being GraphUnion of G1,G2

for v, w being Vertex of G st v <> w holds

ex e being object st e Joins v,w,G

for G2 being GraphComplement of G1

for G being GraphUnion of G1,G2

for v, w being Vertex of G st v <> w holds

ex e being object st e Joins v,w,G

proof end;

registration

let G1 be _Graph;

let G2 be GraphComplement of G1;

coherence

for b_{1} being GraphUnion of G1,G2 holds b_{1} is complete

end;
let G2 be GraphComplement of G1;

coherence

for b

proof end;

registration

let G1 be non-Dmulti _Graph;

let G2 be DLGraphComplement of G1;

coherence

for b_{1} being GraphUnion of G1,G2 holds b_{1} is non-Dmulti

end;
let G2 be DLGraphComplement of G1;

coherence

for b

proof end;

registration

let G1 be non-multi _Graph;

let G2 be LGraphComplement of G1;

coherence

for b_{1} being GraphUnion of G1,G2 holds b_{1} is non-multi

end;
let G2 be LGraphComplement of G1;

coherence

for b

proof end;

registration

let G1 be non-Dmulti _Graph;

let G2 be DGraphComplement of G1;

coherence

for b_{1} being GraphUnion of G1,G2 holds b_{1} is non-Dmulti

end;
let G2 be DGraphComplement of G1;

coherence

for b

proof end;

registration

let G1 be non-multi _Graph;

let G2 be GraphComplement of G1;

coherence

for b_{1} being GraphUnion of G1,G2 holds b_{1} is non-multi

end;
let G2 be GraphComplement of G1;

coherence

for b

proof end;

definition

let S be Graph-membered set ;

end;
attr S is /\-tolerating means :Def27: :: GLIB_014:def 27

( meet (the_Vertices_of S) <> {} & ( for G1, G2 being _Graph st G1 in S & G2 in S holds

G1 tolerates G2 ) );

( meet (the_Vertices_of S) <> {} & ( for G1, G2 being _Graph st G1 in S & G2 in S holds

G1 tolerates G2 ) );

:: deftheorem Def27 defines /\-tolerating GLIB_014:def 27 :

for S being Graph-membered set holds

( S is /\-tolerating iff ( meet (the_Vertices_of S) <> {} & ( for G1, G2 being _Graph st G1 in S & G2 in S holds

G1 tolerates G2 ) ) );

for S being Graph-membered set holds

( S is /\-tolerating iff ( meet (the_Vertices_of S) <> {} & ( for G1, G2 being _Graph st G1 in S & G2 in S holds

G1 tolerates G2 ) ) );

definition

let S be non empty Graph-membered set ;

( S is /\-tolerating iff ( meet (the_Vertices_of S) <> {} & ( for G1, G2 being Element of S holds G1 tolerates G2 ) ) ) ;

end;
redefine attr S is /\-tolerating means :: GLIB_014:def 28

( meet (the_Vertices_of S) <> {} & ( for G1, G2 being Element of S holds G1 tolerates G2 ) );

compatibility ( meet (the_Vertices_of S) <> {} & ( for G1, G2 being Element of S holds G1 tolerates G2 ) );

( S is /\-tolerating iff ( meet (the_Vertices_of S) <> {} & ( for G1, G2 being Element of S holds G1 tolerates G2 ) ) ) ;

:: deftheorem defines /\-tolerating GLIB_014:def 28 :

for S being non empty Graph-membered set holds

( S is /\-tolerating iff ( meet (the_Vertices_of S) <> {} & ( for G1, G2 being Element of S holds G1 tolerates G2 ) ) );

for S being non empty Graph-membered set holds

( S is /\-tolerating iff ( meet (the_Vertices_of S) <> {} & ( for G1, G2 being Element of S holds G1 tolerates G2 ) ) );

theorem Th34: :: GLIB_014:34

for S being Graph-membered set holds

( S is /\-tolerating iff ( S is \/-tolerating & meet (the_Vertices_of S) <> {} ) ) ;

( S is /\-tolerating iff ( S is \/-tolerating & meet (the_Vertices_of S) <> {} ) ) ;

registration
end;

registration

coherence

for b_{1} being Graph-membered set st b_{1} is /\-tolerating holds

( b_{1} is \/-tolerating & not b_{1} is empty )

ex b_{1} being Graph-membered set st b_{1} is /\-tolerating

end;
for b

( b

proof end;

existence ex b

proof end;

theorem Th35: :: GLIB_014:35

for G1, G2 being _Graph holds

( ( G1 tolerates G2 & the_Vertices_of G1 meets the_Vertices_of G2 ) iff {G1,G2} is /\-tolerating )

( ( G1 tolerates G2 & the_Vertices_of G1 meets the_Vertices_of G2 ) iff {G1,G2} is /\-tolerating )

proof end;

theorem :: GLIB_014:36

for S1, S2 being non empty Graph-membered set st S1 \/ S2 is /\-tolerating holds

( S1 is /\-tolerating & S2 is /\-tolerating )

( S1 is /\-tolerating & S2 is /\-tolerating )

proof end;

registration

let S be GraphMeetSet;

coherence

( meet (the_Source_of S) is Function-like & meet (the_Source_of S) is Relation-like ) ;

coherence

( meet (the_Target_of S) is Function-like & meet (the_Target_of S) is Relation-like ) ;

end;
coherence

( meet (the_Source_of S) is Function-like & meet (the_Source_of S) is Relation-like ) ;

coherence

( meet (the_Target_of S) is Function-like & meet (the_Target_of S) is Relation-like ) ;

registration

let S be GraphMeetSet;

coherence

( meet (the_Source_of S) is meet (the_Edges_of S) -defined & meet (the_Source_of S) is meet (the_Vertices_of S) -valued )

( meet (the_Target_of S) is meet (the_Edges_of S) -defined & meet (the_Target_of S) is meet (the_Vertices_of S) -valued )

end;
coherence

( meet (the_Source_of S) is meet (the_Edges_of S) -defined & meet (the_Source_of S) is meet (the_Vertices_of S) -valued )

proof end;

coherence ( meet (the_Target_of S) is meet (the_Edges_of S) -defined & meet (the_Target_of S) is meet (the_Vertices_of S) -valued )

proof end;

registration

let S be GraphMeetSet;

coherence

meet (the_Source_of S) is total

meet (the_Target_of S) is total

end;
coherence

meet (the_Source_of S) is total

proof end;

coherence meet (the_Target_of S) is total

proof end;

:: a.k.a. Graph Intersection, but not to be confused with Intersection Graph

definition

let S be GraphMeetSet;

ex b_{1} being _Graph st

( the_Vertices_of b_{1} = meet (the_Vertices_of S) & the_Edges_of b_{1} = meet (the_Edges_of S) & the_Source_of b_{1} = meet (the_Source_of S) & the_Target_of b_{1} = meet (the_Target_of S) )

end;
mode GraphMeet of S -> _Graph means :Def29: :: GLIB_014:def 29

( the_Vertices_of it = meet (the_Vertices_of S) & the_Edges_of it = meet (the_Edges_of S) & the_Source_of it = meet (the_Source_of S) & the_Target_of it = meet (the_Target_of S) );

existence ( the_Vertices_of it = meet (the_Vertices_of S) & the_Edges_of it = meet (the_Edges_of S) & the_Source_of it = meet (the_Source_of S) & the_Target_of it = meet (the_Target_of S) );

ex b

( the_Vertices_of b

proof end;

:: deftheorem Def29 defines GraphMeet GLIB_014:def 29 :

for S being GraphMeetSet

for b_{2} being _Graph holds

( b_{2} is GraphMeet of S iff ( the_Vertices_of b_{2} = meet (the_Vertices_of S) & the_Edges_of b_{2} = meet (the_Edges_of S) & the_Source_of b_{2} = meet (the_Source_of S) & the_Target_of b_{2} = meet (the_Target_of S) ) );

for S being GraphMeetSet

for b

( b

:: not really needed

::definition

::let S be GraphMeetSet;

::func meet S equals the plain GraphMeet of S;

::end;

:: not proven here (DOM from CARD_3)

:: theorem

:: for S being GraphMeetSet, G being GraphMeet of S

:: holds DOM(the_Source_of S) = dom the_Source_of G &

:: DOM(the_Target_of S) = dom the_Target_of G;

::definition

::let S be GraphMeetSet;

::func meet S equals the plain GraphMeet of S;

::end;

:: not proven here (DOM from CARD_3)

:: theorem

:: for S being GraphMeetSet, G being GraphMeet of S

:: holds DOM(the_Source_of S) = dom the_Source_of G &

:: DOM(the_Target_of S) = dom the_Target_of G;

theorem Th37: :: GLIB_014:37

for S being GraphMeetSet

for G being GraphMeet of S

for H being Element of S holds H is Supergraph of G

for G being GraphMeet of S

for H being Element of S holds H is Supergraph of G

proof end;

theorem Th38: :: GLIB_014:38

for S being GraphMeetSet

for G being GraphMeet of S

for G9 being _Graph holds

( G9 is GraphMeet of S iff G == G9 )

for G being GraphMeet of S

for G9 being _Graph holds

( G9 is GraphMeet of S iff G == G9 )

proof end;

registration
end;

definition

let G1, G2 be _Graph;

( ( G1 tolerates G2 & the_Vertices_of G1 meets the_Vertices_of G2 implies ex b_{1} being Subgraph of G1 ex S being GraphMeetSet st

( S = {G1,G2} & b_{1} is GraphMeet of S ) ) & ( ( not G1 tolerates G2 or not the_Vertices_of G1 meets the_Vertices_of G2 ) implies ex b_{1} being Subgraph of G1 st b_{1} == G1 ) )

for b_{1} being Subgraph of G1 holds verum
;

end;
mode GraphMeet of G1,G2 -> Subgraph of G1 means :Def30: :: GLIB_014:def 30

ex S being GraphMeetSet st

( S = {G1,G2} & it is GraphMeet of S ) if ( G1 tolerates G2 & the_Vertices_of G1 meets the_Vertices_of G2 )

otherwise it == G1;

existence ex S being GraphMeetSet st

( S = {G1,G2} & it is GraphMeet of S ) if ( G1 tolerates G2 & the_Vertices_of G1 meets the_Vertices_of G2 )

otherwise it == G1;

( ( G1 tolerates G2 & the_Vertices_of G1 meets the_Vertices_of G2 implies ex b

( S = {G1,G2} & b

proof end;

consistency for b

:: deftheorem Def30 defines GraphMeet GLIB_014:def 30 :

for G1, G2 being _Graph

for b_{3} being Subgraph of G1 holds

( ( G1 tolerates G2 & the_Vertices_of G1 meets the_Vertices_of G2 implies ( b_{3} is GraphMeet of G1,G2 iff ex S being GraphMeetSet st

( S = {G1,G2} & b_{3} is GraphMeet of S ) ) ) & ( ( not G1 tolerates G2 or not the_Vertices_of G1 meets the_Vertices_of G2 ) implies ( b_{3} is GraphMeet of G1,G2 iff b_{3} == G1 ) ) );

for G1, G2 being _Graph

for b

( ( G1 tolerates G2 & the_Vertices_of G1 meets the_Vertices_of G2 implies ( b

( S = {G1,G2} & b

:: not really needed

::definition

::let G1, G2 be _Graph;

::func G1 /\ G2 equals the plain GraphMeet of G1, G2;

::end;

::definition

::let G1, G2 be _Graph;

::func G1 /\ G2 equals the plain GraphMeet of G1, G2;

::end;

theorem Th40: :: GLIB_014:40

for G1, G2, G being _Graph st G1 tolerates G2 & the_Vertices_of G1 meets the_Vertices_of G2 holds

( G is GraphMeet of G1,G2 iff ( the_Vertices_of G = (the_Vertices_of G1) /\ (the_Vertices_of G2) & the_Edges_of G = (the_Edges_of G1) /\ (the_Edges_of G2) & the_Source_of G = (the_Source_of G1) /\ (the_Source_of G2) & the_Target_of G = (the_Target_of G1) /\ (the_Target_of G2) ) )

( G is GraphMeet of G1,G2 iff ( the_Vertices_of G = (the_Vertices_of G1) /\ (the_Vertices_of G2) & the_Edges_of G = (the_Edges_of G1) /\ (the_Edges_of G2) & the_Source_of G = (the_Source_of G1) /\ (the_Source_of G2) & the_Target_of G = (the_Target_of G1) /\ (the_Target_of G2) ) )

proof end;

theorem Th41: :: GLIB_014:41

for G1, G2 being _Graph

for G being GraphMeet of G1,G2 st G1 tolerates G2 & the_Vertices_of G1 meets the_Vertices_of G2 holds

G is Subgraph of G2

for G being GraphMeet of G1,G2 st G1 tolerates G2 & the_Vertices_of G1 meets the_Vertices_of G2 holds

G is Subgraph of G2

proof end;

theorem :: GLIB_014:42

for G1, G2 being _Graph

for G being GraphMeet of G1,G2 st G1 tolerates G2 & the_Vertices_of G1 meets the_Vertices_of G2 holds

G is GraphMeet of G2,G1

for G being GraphMeet of G1,G2 st G1 tolerates G2 & the_Vertices_of G1 meets the_Vertices_of G2 holds

G is GraphMeet of G2,G1

proof end;

theorem Th43: :: GLIB_014:43

for G1, G2, G9 being _Graph

for G being GraphMeet of G1,G2 holds

( G9 is GraphMeet of G1,G2 iff G == G9 )

for G being GraphMeet of G1,G2 holds

( G9 is GraphMeet of G1,G2 iff G == G9 )

proof end;

registration
end;

theorem Th45: :: GLIB_014:45

for G1, G2 being _Graph

for G being GraphMeet of G1,G2 st the_Vertices_of G1 meets the_Vertices_of G2 & the_Edges_of G1 misses the_Edges_of G2 holds

G is edgeless

for G being GraphMeet of G1,G2 st the_Vertices_of G1 meets the_Vertices_of G2 & the_Edges_of G1 misses the_Edges_of G2 holds

G is edgeless

proof end;

registration

let G1 be _Graph;

let G2 be DLGraphComplement of G1;

coherence

for b_{1} being GraphMeet of G1,G2 holds b_{1} is edgeless

end;
let G2 be DLGraphComplement of G1;

coherence

for b

proof end;

registration

let G1 be _Graph;

let G2 be LGraphComplement of G1;

coherence

for b_{1} being GraphMeet of G1,G2 holds b_{1} is edgeless

end;
let G2 be LGraphComplement of G1;

coherence

for b

proof end;

registration

let G1 be _Graph;

let G2 be DGraphComplement of G1;

coherence

for b_{1} being GraphMeet of G1,G2 holds b_{1} is edgeless

end;
let G2 be DGraphComplement of G1;

coherence

for b

proof end;

registration

let G1 be _Graph;

let G2 be GraphComplement of G1;

coherence

for b_{1} being GraphMeet of G1,G2 holds b_{1} is edgeless

end;
let G2 be GraphComplement of G1;

coherence

for b

proof end;

:: to construct an infinite number of graphs at once