:: About Graph Unions and Intersections
:: by Sebastian Koch
::
:: Received May 19, 2020
:: Copyright (c) 2020-2021 Association of Mizar Users


definition
let X be set ;
attr X is Graph-membered means :Def1: :: GLIB_014:def 1
 for x being object st x in X holds
x is _Graph;
end;

:: 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 );

registration
cluster empty -> Graph-membered for set ;
coherence
for b1 being set st b1 is empty holds
b1 is Graph-membered ;
end;

registration
let F be Graph-yielding Function;
cluster rng F -> Graph-membered ;
coherence
rng F is Graph-membered
proof end;
end;

registration
let G1 be _Graph;
cluster {G1} -> Graph-membered ;
coherence
{G1} is Graph-membered by TARSKI:def 1;
let G2 be _Graph;
cluster {G1,G2} -> Graph-membered ;
coherence
{G1,G2} is Graph-membered
proof end;
end;

:: there is no functor/mode yet
:: to construct an infinite number of graphs at once
registration
cluster empty Graph-membered for set ;
existence
ex b1 being set st
( b1 is empty & b1 is Graph-membered )
proof end;
cluster non empty trivial finite Graph-membered for set ;
existence
ex b1 being set st
( b1 is trivial & b1 is finite & not b1 is empty & b1 is Graph-membered )
proof end;
end;

registration
let X be Graph-membered set ;
cluster -> Graph-membered for Element of K19(X);
coherence
for b1 being Subset of X holds b1 is Graph-membered by Def1;
end;

:: the usual set operations preserve graph membership
registration
let X be Graph-membered set ;
let Y be set ;
cluster X /\ Y -> Graph-membered ;
coherence
X /\ Y is Graph-membered
proof end;
cluster X \ Y -> Graph-membered ;
coherence
X \ Y is Graph-membered ;
end;

registration
let X, Y be Graph-membered set ;
cluster X \/ Y -> Graph-membered ;
coherence
X \/ Y is Graph-membered
proof end;
cluster X \+\ Y -> Graph-membered ;
coherence
X \+\ Y is Graph-membered ;
end;

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
proof end;

theorem :: GLIB_014:2
for X being set st ex Y being Graph-membered set st Y in X holds
meet X is Graph-membered
proof end;

registration
let X be non empty Graph-membered set ;
cluster -> Relation-like Function-like for Element of X;
coherence
for b1 being Element of X holds
( b1 is Function-like & b1 is Relation-like ) by Def1;
end;

registration
let X be non empty Graph-membered set ;
cluster -> NAT -defined finite for Element of X;
coherence
for b1 being Element of X holds
( b1 is NAT -defined & b1 is finite ) by Def1;
end;

registration
let X be non empty Graph-membered set ;
cluster -> [Graph-like] for Element of X;
coherence
for b1 being Element of X holds b1 is [Graph-like] by Def1;
end;

:: several graphs attributes for sets of graphs
:: ("finite" and "trivial" are deliberately omitted,
:: so that the set attributes are not overridden)
definition
let S be Graph-membered set ;
attr S is plain means :Def2: :: GLIB_014:def 2
 for G being _Graph st G in S holds
G is plain ;
attr S is loopless means :Def3: :: GLIB_014:def 3
 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 ;
attr S is non-Dmulti means :Def5: :: GLIB_014:def 5
 for G being _Graph st G in S holds
G is non-Dmulti ;
attr S is simple means :: GLIB_014:def 6
 for G being _Graph st G in S holds
G is simple ;
attr S is Dsimple means :: GLIB_014:def 7
 for G being _Graph st G in S holds
G is Dsimple ;
attr S is acyclic means :Def8: :: GLIB_014:def 8
 for G being _Graph st G in S holds
G is acyclic ;
attr S is connected means :Def9: :: GLIB_014:def 9
 for G being _Graph st G in S holds
G is connected ;
attr S is Tree-like means :: GLIB_014:def 10
 for G being _Graph st G in S holds
G is Tree-like ;
attr S is chordal means :Def11: :: GLIB_014:def 11
 for G being _Graph st G in S holds
G is chordal ;
attr S is edgeless means :Def12: :: GLIB_014:def 12
 for G being _Graph st G in S holds
G is edgeless ;
attr S is loopfull means :Def13: :: GLIB_014:def 13
 for G being _Graph st G in S holds
G is loopfull ;
end;

:: 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 );

:: 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 );

:: 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 );

:: 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 );

:: 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 );

:: 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 );

:: 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 );

:: 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 );

:: 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 );

:: 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 );

:: 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 );

:: 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 );

:: negative clustering are omitted, because
:: negative attributes (e.g. "non-loopless") are not defined yet
registration
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 b1 being Graph-membered set st b1 is empty holds
( b1 is plain & b1 is loopless & b1 is non-multi & b1 is non-Dmulti & b1 is simple & b1 is Dsimple & b1 is acyclic & b1 is connected & b1 is Tree-like & b1 is chordal & b1 is edgeless & b1 is loopfull ) ;
cluster Graph-membered non-multi -> Graph-membered non-Dmulti for set ;
coherence
for b1 being Graph-membered set st b1 is non-multi holds
b1 is non-Dmulti
proof end;
cluster Graph-membered loopless non-multi -> Graph-membered simple for set ;
coherence
for b1 being Graph-membered set st b1 is loopless & b1 is non-multi holds
b1 is simple
proof end;
cluster Graph-membered loopless non-Dmulti -> Graph-membered Dsimple for set ;
coherence
for b1 being Graph-membered set st b1 is loopless & b1 is non-Dmulti holds
b1 is Dsimple
proof end;
cluster Graph-membered simple -> Graph-membered loopless non-multi for set ;
coherence
for b1 being Graph-membered set st b1 is simple holds
( b1 is loopless & b1 is non-multi )
proof end;
cluster Graph-membered Dsimple -> Graph-membered loopless non-Dmulti for set ;
coherence
for b1 being Graph-membered set st b1 is Dsimple holds
( b1 is loopless & b1 is non-Dmulti )
proof end;
cluster Graph-membered acyclic -> Graph-membered simple for set ;
coherence
for b1 being Graph-membered set st b1 is acyclic holds
b1 is simple
proof end;
cluster Graph-membered acyclic connected -> Graph-membered Tree-like for set ;
coherence
for b1 being Graph-membered set st b1 is acyclic & b1 is connected holds
b1 is Tree-like
proof end;
cluster Graph-membered Tree-like -> Graph-membered acyclic connected for set ;
coherence
for b1 being Graph-membered set st b1 is Tree-like holds
( b1 is acyclic & b1 is connected )
proof end;
end;

registration
let G1 be plain _Graph;
cluster {G1} -> plain ;
coherence
{G1} is plain by TARSKI:def 1;
let G2 be plain _Graph;
cluster {G1,G2} -> plain ;
coherence
{G1,G2} is plain
proof end;
end;

registration
let G1 be loopless _Graph;
cluster {G1} -> loopless ;
coherence
{G1} is loopless by TARSKI:def 1;
let G2 be loopless _Graph;
cluster {G1,G2} -> loopless ;
coherence
{G1,G2} is loopless
proof end;
end;

registration
let G1 be non-multi _Graph;
cluster {G1} -> non-multi ;
coherence
{G1} is non-multi by TARSKI:def 1;
let G2 be non-multi _Graph;
cluster {G1,G2} -> non-multi ;
coherence
{G1,G2} is non-multi
proof end;
end;

registration
let G1 be non-Dmulti _Graph;
cluster {G1} -> non-Dmulti ;
coherence
{G1} is non-Dmulti by TARSKI:def 1;
let G2 be non-Dmulti _Graph;
cluster {G1,G2} -> non-Dmulti ;
coherence
{G1,G2} is non-Dmulti
proof end;
end;

registration
let G1 be simple _Graph;
cluster {G1} -> simple ;
coherence
{G1} is simple ;
let G2 be simple _Graph;
cluster {G1,G2} -> simple ;
coherence
{G1,G2} is simple ;
end;

registration
let G1 be Dsimple _Graph;
cluster {G1} -> Dsimple ;
coherence
{G1} is Dsimple ;
let G2 be Dsimple _Graph;
cluster {G1,G2} -> Dsimple ;
coherence
{G1,G2} is Dsimple ;
end;

registration
let G1 be acyclic _Graph;
cluster {G1} -> acyclic ;
coherence
{G1} is acyclic by TARSKI:def 1;
let G2 be acyclic _Graph;
cluster {G1,G2} -> acyclic ;
coherence
{G1,G2} is acyclic
proof end;
end;

registration
let G1 be connected _Graph;
cluster {G1} -> connected ;
coherence
{G1} is connected by TARSKI:def 1;
let G2 be connected _Graph;
cluster {G1,G2} -> connected ;
coherence
{G1,G2} is connected
proof end;
end;

registration
let G1 be Tree-like _Graph;
cluster {G1} -> Tree-like ;
coherence
{G1} is Tree-like ;
let G2 be Tree-like _Graph;
cluster {G1,G2} -> Tree-like ;
coherence
{G1,G2} is Tree-like ;
end;

registration
let G1 be chordal _Graph;
cluster {G1} -> chordal ;
coherence
{G1} is chordal by TARSKI:def 1;
let G2 be chordal _Graph;
cluster {G1,G2} -> chordal ;
coherence
{G1,G2} is chordal
proof end;
end;

registration
let G1 be edgeless _Graph;
cluster {G1} -> edgeless ;
coherence
{G1} is edgeless by TARSKI:def 1;
let G2 be edgeless _Graph;
cluster {G1,G2} -> edgeless ;
coherence
{G1,G2} is edgeless
proof end;
end;

registration
let G1 be loopfull _Graph;
cluster {G1} -> loopfull ;
coherence
{G1} is loopfull by TARSKI:def 1;
let G2 be loopfull _Graph;
cluster {G1,G2} -> loopfull ;
coherence
{G1,G2} is loopfull
proof end;
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
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 ) )
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 ) )
proof end;

registration
let F be Graph-yielding plain Function;
cluster rng F -> plain ;
coherence
rng F is plain by Th3;
end;

registration
let F be Graph-yielding loopless Function;
cluster rng F -> loopless ;
coherence
rng F is loopless by Th3;
end;

registration
let F be Graph-yielding non-multi Function;
cluster rng F -> non-multi ;
coherence
rng F is non-multi by Th3;
end;

registration
let F be Graph-yielding non-Dmulti Function;
cluster rng F -> non-Dmulti ;
coherence
rng F is non-Dmulti by Th3;
end;

registration
let F be Graph-yielding simple Function;
cluster rng F -> simple ;
coherence
rng F is simple ;
end;

registration
let F be Graph-yielding Dsimple Function;
cluster rng F -> Dsimple ;
coherence
rng F is Dsimple ;
end;

registration
let F be Graph-yielding acyclic Function;
cluster rng F -> acyclic ;
coherence
rng F is acyclic by Th3;
end;

registration
let F be Graph-yielding connected Function;
cluster rng F -> connected ;
coherence
rng F is connected by Th3;
end;

registration
let F be Graph-yielding Tree-like Function;
cluster rng F -> Tree-like ;
coherence
rng F is Tree-like ;
end;

registration
let F be Graph-yielding chordal Function;
cluster rng F -> chordal ;
coherence
rng F is chordal by Th3;
end;

registration
let F be Graph-yielding edgeless Function;
cluster rng F -> edgeless ;
coherence
rng F is edgeless by Th3;
end;

registration
let F be Graph-yielding loopfull Function;
cluster rng F -> loopfull ;
coherence
rng F is loopfull by Th3;
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
registration
let X be Graph-membered plain set ;
cluster -> plain for Element of K19(X);
coherence
for b1 being Subset of X holds b1 is plain by Def2;
end;

registration
let X be Graph-membered loopless set ;
cluster -> loopless for Element of K19(X);
coherence
for b1 being Subset of X holds b1 is loopless by Def3;
end;

registration
let X be Graph-membered non-multi set ;
cluster -> non-multi for Element of K19(X);
coherence
for b1 being Subset of X holds b1 is non-multi by Def4;
end;

registration
let X be Graph-membered non-Dmulti set ;
cluster -> non-Dmulti for Element of K19(X);
coherence
for b1 being Subset of X holds b1 is non-Dmulti by Def5;
end;

registration
let X be Graph-membered simple set ;
cluster -> simple for Element of K19(X);
coherence
for b1 being Subset of X holds b1 is simple ;
end;

registration
let X be Graph-membered Dsimple set ;
cluster -> Dsimple for Element of K19(X);
coherence
for b1 being Subset of X holds b1 is Dsimple ;
end;

registration
let X be Graph-membered acyclic set ;
cluster -> acyclic for Element of K19(X);
coherence
for b1 being Subset of X holds b1 is acyclic by Def8;
end;

registration
let X be Graph-membered connected set ;
cluster -> connected for Element of K19(X);
coherence
for b1 being Subset of X holds b1 is connected by Def9;
end;

registration
let X be Graph-membered Tree-like set ;
cluster -> Tree-like for Element of K19(X);
coherence
for b1 being Subset of X holds b1 is Tree-like ;
end;

registration
let X be Graph-membered chordal set ;
cluster -> chordal for Element of K19(X);
coherence
for b1 being Subset of X holds b1 is chordal by Def11;
end;

registration
let X be Graph-membered edgeless set ;
cluster -> edgeless for Element of K19(X);
coherence
for b1 being Subset of X holds b1 is edgeless by Def12;
end;

registration
let X be Graph-membered loopfull set ;
cluster -> loopfull for Element of K19(X);
coherence
for b1 being Subset of X holds b1 is loopfull by Def13;
end;

::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
registration
let X be Graph-membered plain set ;
let Y be set ;
cluster X /\ Y -> plain ;
coherence
X /\ Y is plain
proof end;
cluster X \ Y -> plain ;
coherence
X \ Y is plain ;
end;

registration
let X, Y be Graph-membered plain set ;
cluster X \/ Y -> plain ;
coherence
X \/ Y is plain
proof end;
cluster X \+\ Y -> plain ;
coherence
X \+\ Y is plain ;
end;

registration
let X be Graph-membered loopless set ;
let Y be set ;
cluster X /\ Y -> loopless ;
coherence
X /\ Y is loopless
proof end;
cluster X \ Y -> loopless ;
coherence
X \ Y is loopless ;
end;

registration
let X, Y be Graph-membered loopless set ;
cluster X \/ Y -> loopless ;
coherence
X \/ Y is loopless
proof end;
cluster X \+\ Y -> loopless ;
coherence
X \+\ Y is loopless ;
end;

registration
let X be Graph-membered non-multi set ;
let Y be set ;
cluster X /\ Y -> non-multi ;
coherence
X /\ Y is non-multi
proof end;
cluster X \ Y -> non-multi ;
coherence
X \ Y is non-multi ;
end;

registration
let X, Y be Graph-membered non-multi set ;
cluster X \/ Y -> non-multi ;
coherence
X \/ Y is non-multi
proof end;
cluster X \+\ Y -> non-multi ;
coherence
X \+\ Y is non-multi ;
end;

registration
let X be Graph-membered non-Dmulti set ;
let Y be set ;
cluster X /\ Y -> non-Dmulti ;
coherence
X /\ Y is non-Dmulti
proof end;
cluster X \ Y -> non-Dmulti ;
coherence
X \ Y is non-Dmulti ;
end;

registration
let X, Y be Graph-membered non-Dmulti set ;
cluster X \/ Y -> non-Dmulti ;
coherence
X \/ Y is non-Dmulti
proof end;
cluster X \+\ Y -> non-Dmulti ;
coherence
X \+\ Y is non-Dmulti ;
end;

registration
let X be Graph-membered simple set ;
let Y be set ;
cluster X /\ Y -> simple ;
coherence
X /\ Y is simple ;
cluster X \ Y -> simple ;
coherence
X \ Y is simple ;
end;

registration
let X, Y be Graph-membered simple set ;
cluster X \/ Y -> simple ;
coherence
X \/ Y is simple ;
cluster X \+\ Y -> simple ;
coherence
X \+\ Y is simple ;
end;

registration
let X be Graph-membered Dsimple set ;
let Y be set ;
cluster X /\ Y -> Dsimple ;
coherence
X /\ Y is Dsimple ;
cluster X \ Y -> Dsimple ;
coherence
X \ Y is Dsimple ;
end;

registration
let X, Y be Graph-membered Dsimple set ;
cluster X \/ Y -> Dsimple ;
coherence
X \/ Y is Dsimple ;
cluster X \+\ Y -> Dsimple ;
coherence
X \+\ Y is Dsimple ;
end;

registration
let X be Graph-membered acyclic set ;
let Y be set ;
cluster X /\ Y -> acyclic ;
coherence
X /\ Y is acyclic
proof end;
cluster X \ Y -> acyclic ;
coherence
X \ Y is acyclic ;
end;

registration
let X, Y be Graph-membered acyclic set ;
cluster X \/ Y -> acyclic ;
coherence
X \/ Y is acyclic
proof end;
cluster X \+\ Y -> acyclic ;
coherence
X \+\ Y is acyclic ;
end;

registration
let X be Graph-membered connected set ;
let Y be set ;
cluster X /\ Y -> connected ;
coherence
X /\ Y is connected
proof end;
cluster X \ Y -> connected ;
coherence
X \ Y is connected ;
end;

registration
let X, Y be Graph-membered connected set ;
cluster X \/ Y -> connected ;
coherence
X \/ Y is connected
proof end;
cluster X \+\ Y -> connected ;
coherence
X \+\ Y is connected ;
end;

registration
let X be Graph-membered Tree-like set ;
let Y be set ;
cluster X /\ Y -> Tree-like ;
coherence
X /\ Y is Tree-like ;
cluster X \ Y -> Tree-like ;
coherence
X \ Y is Tree-like ;
end;

registration
let X, Y be Graph-membered Tree-like set ;
cluster X \/ Y -> Tree-like ;
coherence
X \/ Y is Tree-like ;
cluster X \+\ Y -> Tree-like ;
coherence
X \+\ Y is Tree-like ;
end;

registration
let X be Graph-membered chordal set ;
let Y be set ;
cluster X /\ Y -> chordal ;
coherence
X /\ Y is chordal
proof end;
cluster X \ Y -> chordal ;
coherence
X \ Y is chordal ;
end;

registration
let X, Y be Graph-membered chordal set ;
cluster X \/ Y -> chordal ;
coherence
X \/ Y is chordal
proof end;
cluster X \+\ Y -> chordal ;
coherence
X \+\ Y is chordal ;
end;

registration
let X be Graph-membered edgeless set ;
let Y be set ;
cluster X /\ Y -> edgeless ;
coherence
X /\ Y is edgeless
proof end;
cluster X \ Y -> edgeless ;
coherence
X \ Y is edgeless ;
end;

registration
let X, Y be Graph-membered edgeless set ;
cluster X \/ Y -> edgeless ;
coherence
X \/ Y is edgeless
proof end;
cluster X \+\ Y -> edgeless ;
coherence
X \+\ Y is edgeless ;
end;

registration
let X be Graph-membered loopfull set ;
let Y be set ;
cluster X /\ Y -> loopfull ;
coherence
X /\ Y is loopfull
proof end;
cluster X \ Y -> loopfull ;
coherence
X \ Y is loopfull ;
end;

registration
let X, Y be Graph-membered loopfull set ;
cluster X \/ Y -> loopfull ;
coherence
X \/ Y is loopfull
proof end;
cluster X \+\ Y -> loopfull ;
coherence
X \+\ Y is loopfull ;
end;

::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
registration
cluster empty Graph-membered plain loopless non-multi non-Dmulti simple Dsimple acyclic connected Tree-like chordal edgeless loopfull for set ;
existence
ex b1 being Graph-membered set st
( b1 is empty & b1 is plain & b1 is loopless & b1 is non-multi & b1 is non-Dmulti & b1 is simple & b1 is Dsimple & b1 is acyclic & b1 is connected & b1 is Tree-like & b1 is chordal & b1 is edgeless & b1 is loopfull )
proof end;
cluster non empty Graph-membered loopless non-multi non-Dmulti simple Dsimple acyclic connected Tree-like for set ;
existence
ex b1 being Graph-membered set st
( not b1 is empty & b1 is Tree-like & b1 is acyclic & b1 is connected & b1 is simple & b1 is Dsimple & b1 is loopless & b1 is non-multi & b1 is non-Dmulti )
proof end;
cluster non empty Graph-membered chordal edgeless for set ;
existence
ex b1 being Graph-membered set st
( not b1 is empty & b1 is edgeless & b1 is chordal )
proof end;
cluster non empty Graph-membered loopfull for set ;
existence
ex b1 being Graph-membered set st
( not b1 is empty & b1 is loopfull )
proof end;
cluster non empty Graph-membered plain for set ;
existence
ex b1 being Graph-membered set st
( not b1 is empty & b1 is plain )
proof end;
end;

registration
let S be non empty Graph-membered plain set ;
cluster -> plain for Element of S;
coherence
for b1 being Element of S holds b1 is plain by Def2;
end;

registration
let S be non empty Graph-membered loopless set ;
cluster -> loopless for Element of S;
coherence
for b1 being Element of S holds b1 is loopless by Def3;
end;

registration
let S be non empty Graph-membered non-multi set ;
cluster -> non-multi for Element of S;
coherence
for b1 being Element of S holds b1 is non-multi by Def4;
end;

registration
let S be non empty Graph-membered non-Dmulti set ;
cluster -> non-Dmulti for Element of S;
coherence
for b1 being Element of S holds b1 is non-Dmulti by Def5;
end;

registration
let S be non empty Graph-membered simple set ;
cluster -> simple for Element of S;
coherence
for b1 being Element of S holds b1 is simple ;
end;

registration
let S be non empty Graph-membered Dsimple set ;
cluster -> Dsimple for Element of S;
coherence
for b1 being Element of S holds b1 is Dsimple ;
end;

registration
let S be non empty Graph-membered acyclic set ;
cluster -> acyclic for Element of S;
coherence
for b1 being Element of S holds b1 is acyclic by Def8;
end;

registration
let S be non empty Graph-membered connected set ;
cluster -> connected for Element of S;
coherence
for b1 being Element of S holds b1 is connected by Def9;
end;

registration
let S be non empty Graph-membered Tree-like set ;
cluster -> Tree-like for Element of S;
coherence
for b1 being Element of S holds b1 is Tree-like ;
end;

registration
let S be non empty Graph-membered chordal set ;
cluster -> chordal for Element of S;
coherence
for b1 being Element of S holds b1 is chordal by Def11;
end;

registration
let S be non empty Graph-membered edgeless set ;
cluster -> edgeless for Element of S;
coherence
for b1 being Element of S holds b1 is edgeless by Def12;
end;

registration
let S be non empty Graph-membered loopfull set ;
cluster -> loopfull for Element of S;
coherence
for b1 being Element of S holds b1 is loopfull by Def13;
end;

::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
definition
let S be Graph-membered set ;
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
ex b1 being set st
for V being object holds
( V in b1 iff ex G being _Graph st
( G in S & V = the_Vertices_of G ) )
proof end;
uniqueness
for b1, b2 being set st ( for V being object holds
( V in b1 iff ex G being _Graph st
( G in S & V = the_Vertices_of G ) ) ) & ( for V being object holds
( V in b2 iff ex G being _Graph st
( G in S & V = the_Vertices_of G ) ) ) holds
b1 = b2
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
ex b1 being set st
for E being object holds
( E in b1 iff ex G being _Graph st
( G in S & E = the_Edges_of G ) )
proof end;
uniqueness
for b1, b2 being set st ( for E being object holds
( E in b1 iff ex G being _Graph st
( G in S & E = the_Edges_of G ) ) ) & ( for E being object holds
( E in b2 iff ex G being _Graph st
( G in S & E = the_Edges_of G ) ) ) holds
b1 = b2
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
ex b1 being set st
for s being object holds
( s in b1 iff ex G being _Graph st
( G in S & s = the_Source_of G ) )
proof end;
uniqueness
for b1, b2 being set st ( for s being object holds
( s in b1 iff ex G being _Graph st
( G in S & s = the_Source_of G ) ) ) & ( for s being object holds
( s in b2 iff ex G being _Graph st
( G in S & s = the_Source_of G ) ) ) holds
b1 = b2
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
ex b1 being set st
for t being object holds
( t in b1 iff ex G being _Graph st
( G in S & t = the_Target_of G ) )
proof end;
uniqueness
for b1, b2 being set st ( for t being object holds
( t in b1 iff ex G being _Graph st
( G in S & t = the_Target_of G ) ) ) & ( for t being object holds
( t in b2 iff ex G being _Graph st
( G in S & t = the_Target_of G ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def14 defines the_Vertices_of GLIB_014:def 14 :
for S being Graph-membered set
for b2 being set holds
( b2 = the_Vertices_of S iff for V being object holds
( V in b2 iff ex G being _Graph st
( 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 b2 being set holds
( b2 = the_Edges_of S iff for E being object holds
( E in b2 iff ex G being _Graph st
( 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 b2 being set holds
( b2 = the_Source_of S iff for s being object holds
( s in b2 iff ex G being _Graph st
( 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 b2 being set holds
( b2 = the_Target_of S iff for t being object holds
( t in b2 iff ex G being _Graph st
( G in S & t = the_Target_of G ) ) );

definition
let S be non empty Graph-membered set ;
redefine func the_Vertices_of S equals :: GLIB_014:def 18
 { (the_Vertices_of G) where G is Element of S : verum } ;
compatibility
for b1 being set holds
( b1 = the_Vertices_of S iff b1 = { (the_Vertices_of G) where G is Element of S : verum } )
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
for b1 being set holds
( b1 = the_Edges_of S iff b1 = { (the_Edges_of G) where G is Element of S : verum } )
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
for b1 being set holds
( b1 = the_Source_of S iff b1 = { (the_Source_of G) where G is Element of S : verum } )
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
for b1 being set holds
( b1 = the_Target_of S iff b1 = { (the_Target_of G) where G is Element of S : verum } )
proof end;
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 } ;

:: 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 } ;

:: 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 } ;

:: 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 } ;

registration
let S be non empty Graph-membered set ;
cluster union (the_Vertices_of S) -> non empty ;
coherence
not union (the_Vertices_of S) is empty
proof end;
end;

registration
let S be Graph-membered set ;
cluster the_Source_of S -> functional ;
coherence
the_Source_of S is functional
proof end;
cluster the_Target_of S -> functional ;
coherence
the_Target_of S is functional
proof end;
end;

registration
let S be empty Graph-membered set ;
cluster the_Vertices_of S -> empty ;
coherence
the_Vertices_of S is empty
proof end;
cluster the_Edges_of S -> empty ;
coherence
the_Edges_of S is empty
proof end;
cluster the_Source_of S -> empty ;
coherence
the_Source_of S is empty
proof end;
cluster the_Target_of S -> empty ;
coherence
the_Target_of S is empty
proof end;
end;

registration
let S be non empty Graph-membered set ;
cluster the_Vertices_of S -> non empty ;
coherence
not the_Vertices_of S is empty
proof end;
cluster the_Edges_of S -> non empty ;
coherence
not the_Edges_of S is empty
proof end;
cluster the_Source_of S -> non empty ;
coherence
not the_Source_of S is empty
proof end;
cluster the_Target_of S -> non empty ;
coherence
not the_Target_of S is empty
proof end;
end;

registration
let S be trivial Graph-membered set ;
cluster the_Vertices_of S -> trivial ;
coherence
the_Vertices_of S is trivial
proof end;
cluster the_Edges_of S -> trivial ;
coherence
the_Edges_of S is trivial
proof end;
cluster the_Source_of S -> trivial ;
coherence
the_Source_of S is trivial
proof end;
cluster the_Target_of S -> trivial ;
coherence
the_Target_of S is trivial
proof end;
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)} )
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)} )
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 )
proof end;

registration
let S be finite Graph-membered set ;
cluster the_Vertices_of S -> finite ;
coherence
the_Vertices_of S is finite
proof end;
cluster the_Edges_of S -> finite ;
coherence
the_Edges_of S is finite
proof end;
cluster the_Source_of S -> finite ;
coherence
the_Source_of S is finite
proof end;
cluster the_Target_of S -> finite ;
coherence
the_Target_of S is finite
proof end;
end;

registration
let S be Graph-membered edgeless set ;
cluster union (the_Edges_of S) -> empty ;
coherence
union (the_Edges_of S) is empty
proof end;
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) )
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) )
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) )
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) )
proof end;

definition
let G1, G2 be _Graph;
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
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;

:: 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 ) );

theorem Th12: :: GLIB_014:12
for G1, G2 being _Graph st the_Edges_of G1 misses the_Edges_of G2 holds
G1 tolerates G2
proof end;

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;

theorem Th14: :: GLIB_014:14
for G1 being _Graph
for G2, G3 being Subgraph of G1 holds G2 tolerates G3
proof end;

theorem Th15: :: GLIB_014:15
for G1 being _Graph
for G2 being Subgraph of G1 holds G1 tolerates G2
proof end;

theorem :: GLIB_014:16
for G1, G2 being _Graph st G1 == G2 holds
G1 tolerates G2
proof end;

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 ) )
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() )
proof end;

definition
let S be Graph-membered set ;
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;
end;

:: 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 );

definition
let S be non empty Graph-membered set ;
redefine attr S is \/-tolerating means :: GLIB_014:def 24
 for G1, G2 being Element of S holds G1 tolerates G2;
compatibility
( S is \/-tolerating iff for G1, G2 being Element of S holds G1 tolerates G2 ) ;
end;

:: 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 );

registration
cluster empty Graph-membered -> Graph-membered \/-tolerating for set ;
coherence
for b1 being Graph-membered set st b1 is empty holds
b1 is \/-tolerating ;
let G be _Graph;
cluster {G} -> \/-tolerating ;
coherence
{G} is \/-tolerating
proof end;
end;

registration
cluster non empty Graph-membered \/-tolerating for set ;
existence
ex b1 being Graph-membered set st
( not b1 is empty & b1 is \/-tolerating )
proof end;
end;

definition
mode GraphUnionSet is non empty Graph-membered \/-tolerating set ;
end;

theorem Th19: :: GLIB_014:19
for G1, G2 being _Graph holds
( G1 tolerates G2 iff {G1,G2} is \/-tolerating )
proof end;

registration
let S1 be Graph-membered \/-tolerating set ;
let S2 be set ;
cluster S1 /\ S2 -> \/-tolerating ;
coherence
S1 /\ S2 is \/-tolerating
proof end;
cluster S1 \ S2 -> \/-tolerating ;
coherence
S1 \ S2 is \/-tolerating by Def23;
end;

theorem Th20: :: GLIB_014:20
for S1, S2 being Graph-membered set st S1 \/ S2 is \/-tolerating holds
( S1 is \/-tolerating & S2 is \/-tolerating )
proof end;

registration
let S be Graph-membered \/-tolerating set ;
cluster the_Source_of S -> compatible ;
coherence
the_Source_of S is compatible
proof end;
cluster the_Target_of S -> compatible ;
coherence
the_Target_of S is compatible
proof end;
end;

registration
let S be Graph-membered \/-tolerating set ;
cluster union (the_Source_of S) -> Relation-like Function-like ;
coherence
( union (the_Source_of S) is Function-like & union (the_Source_of S) is Relation-like ) ;
cluster union (the_Target_of S) -> Relation-like Function-like ;
coherence
( union (the_Target_of S) is Function-like & union (the_Target_of S) is Relation-like ) ;
end;

registration
let S be Graph-membered \/-tolerating set ;
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;
end;

registration
let S be Graph-membered \/-tolerating set ;
cluster union (the_Source_of S) -> total ;
coherence
union (the_Source_of S) is total
proof end;
cluster union (the_Target_of S) -> total ;
coherence
union (the_Target_of S) is total
proof end;
end;

definition
let S be GraphUnionSet;
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
ex b1 being _Graph st
( the_Vertices_of b1 = union (the_Vertices_of S) & the_Edges_of b1 = union (the_Edges_of S) & the_Source_of b1 = union (the_Source_of S) & the_Target_of b1 = union (the_Target_of S) )
proof end;
end;

:: deftheorem Def25 defines GraphUnion GLIB_014:def 25 :
for S being GraphUnionSet
for b2 being _Graph holds
( b2 is GraphUnion of S iff ( the_Vertices_of b2 = union (the_Vertices_of S) & the_Edges_of b2 = union (the_Edges_of S) & the_Source_of b2 = union (the_Source_of S) & the_Target_of b2 = union (the_Target_of S) ) );

:: 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;
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
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 )
proof end;

registration
let S be GraphUnionSet;
cluster Relation-like NAT -defined Function-like finite [Graph-like] plain for GraphUnion of S;
existence
ex b1 being GraphUnion of S st b1 is plain
proof end;
end;

registration
cluster non empty Graph-membered loopless \/-tolerating for set ;
existence
ex b1 being GraphUnionSet st b1 is loopless
proof end;
cluster non empty Graph-membered edgeless \/-tolerating for set ;
existence
ex b1 being GraphUnionSet st b1 is edgeless
proof end;
cluster non empty Graph-membered loopfull \/-tolerating for set ;
existence
ex b1 being GraphUnionSet st b1 is loopfull
proof end;
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 ) )
proof end;

registration
let S be loopless GraphUnionSet;
cluster -> loopless for GraphUnion of S;
coherence
for b1 being GraphUnion of S holds b1 is loopless by Th23;
end;

registration
let S be edgeless GraphUnionSet;
cluster -> edgeless for GraphUnion of S;
coherence
for b1 being GraphUnion of S holds b1 is edgeless by Th23;
end;

registration
let S be loopfull GraphUnionSet;
cluster -> loopfull for GraphUnion of S;
coherence
for b1 being GraphUnion of S holds b1 is loopfull by Th23;
end;

theorem :: GLIB_014:24
for G, H being _Graph holds
( G is GraphUnion of {H} iff G == H )
proof end;

definition
let G1, G2 be _Graph;
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
( ( G1 tolerates G2 implies ex b1 being Supergraph of G1 ex S being GraphUnionSet st
( S = {G1,G2} & b1 is GraphUnion of S ) ) & ( not G1 tolerates G2 implies ex b1 being Supergraph of G1 st b1 == G1 ) )
proof end;
consistency
for b1 being Supergraph of G1 holds verum ;
end;

:: deftheorem Def26 defines GraphUnion GLIB_014:def 26 :
for G1, G2 being _Graph
for b3 being Supergraph of G1 holds
( ( G1 tolerates G2 implies ( b3 is GraphUnion of G1,G2 iff ex S being GraphUnionSet st
( S = {G1,G2} & b3 is GraphUnion of S ) ) ) & ( not G1 tolerates G2 implies ( b3 is GraphUnion of G1,G2 iff b3 == G1 ) ) );

:: not really needed
::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) ) )
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
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
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 )
proof end;

registration
let G1, G2 be _Graph;
cluster Relation-like NAT -defined Function-like finite [Graph-like] plain for GraphUnion of G1,G2;
existence
ex b1 being GraphUnion of G1,G2 st b1 is plain
proof end;
end;

theorem :: GLIB_014:29
for G, G1 being _Graph
for G2 being Subgraph of G1 holds
( G is GraphUnion of G1,G2 iff G == G1 )
proof end;

registration
let G1, G2 be loopless _Graph;
cluster -> loopless for GraphUnion of G1,G2;
coherence
for b1 being GraphUnion of G1,G2 holds b1 is loopless
proof end;
end;

registration
let G1, G2 be edgeless _Graph;
cluster -> edgeless for GraphUnion of G1,G2;
coherence
for b1 being GraphUnion of G1,G2 holds b1 is edgeless
proof end;
end;

registration
let G1, G2 be loopfull _Graph;
cluster -> loopfull for GraphUnion of G1,G2;
coherence
for b1 being GraphUnion of G1,G2 holds b1 is loopfull
proof end;
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
proof end;

registration
let G1 be _Graph;
let G2 be DLGraphComplement of G1;
cluster -> complete loopfull for GraphUnion of G1,G2;
coherence
for b1 being GraphUnion of G1,G2 holds
( b1 is loopfull & b1 is complete )
proof end;
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
proof end;

registration
let G1 be _Graph;
let G2 be LGraphComplement of G1;
cluster -> complete loopfull for GraphUnion of G1,G2;
coherence
for b1 being GraphUnion of G1,G2 holds
( b1 is loopfull & b1 is complete )
proof end;
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
proof end;

registration
let G1 be _Graph;
let G2 be DGraphComplement of G1;
cluster -> complete for GraphUnion of G1,G2;
coherence
for b1 being GraphUnion of G1,G2 holds b1 is complete
proof end;
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
proof end;

registration
let G1 be _Graph;
let G2 be GraphComplement of G1;
cluster -> complete for GraphUnion of G1,G2;
coherence
for b1 being GraphUnion of G1,G2 holds b1 is complete
proof end;
end;

registration
let G1 be non-Dmulti _Graph;
let G2 be DLGraphComplement of G1;
cluster -> non-Dmulti for GraphUnion of G1,G2;
coherence
for b1 being GraphUnion of G1,G2 holds b1 is non-Dmulti
proof end;
end;

registration
let G1 be non-multi _Graph;
let G2 be LGraphComplement of G1;
cluster -> non-multi for GraphUnion of G1,G2;
coherence
for b1 being GraphUnion of G1,G2 holds b1 is non-multi
proof end;
end;

registration
let G1 be non-Dmulti _Graph;
let G2 be DGraphComplement of G1;
cluster -> non-Dmulti for GraphUnion of G1,G2;
coherence
for b1 being GraphUnion of G1,G2 holds b1 is non-Dmulti
proof end;
end;

registration
let G1 be non-multi _Graph;
let G2 be GraphComplement of G1;
cluster -> non-multi for GraphUnion of G1,G2;
coherence
for b1 being GraphUnion of G1,G2 holds b1 is non-multi
proof end;
end;

definition
let S be Graph-membered set ;
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 ) );
end;

:: 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 ) ) );

definition
let S be non empty Graph-membered set ;
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
( S is /\-tolerating iff ( meet (the_Vertices_of S) <> {} & ( for G1, G2 being Element of S holds G1 tolerates G2 ) ) ) ;
end;

:: 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 ) ) );

theorem Th34: :: GLIB_014:34
for S being Graph-membered set holds
( S is /\-tolerating iff ( S is \/-tolerating & meet (the_Vertices_of S) <> {} ) ) ;

registration
let G be _Graph;
cluster {G} -> /\-tolerating ;
coherence
{G} is /\-tolerating
proof end;
end;

registration
cluster Graph-membered /\-tolerating -> non empty Graph-membered \/-tolerating for set ;
coherence
for b1 being Graph-membered set st b1 is /\-tolerating holds
( b1 is \/-tolerating & not b1 is empty )
proof end;
cluster Graph-membered /\-tolerating for set ;
existence
ex b1 being Graph-membered set st b1 is /\-tolerating
proof end;
end;

definition
mode GraphMeetSet is Graph-membered /\-tolerating set ;
end;

registration
let S be GraphMeetSet;
cluster meet (the_Vertices_of S) -> non empty ;
coherence
not meet (the_Vertices_of S) is empty by Def27;
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 )
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 )
proof end;

registration
let S be GraphMeetSet;
cluster meet (the_Source_of S) -> Relation-like Function-like ;
coherence
( meet (the_Source_of S) is Function-like & meet (the_Source_of S) is Relation-like ) ;
cluster meet (the_Target_of S) -> Relation-like Function-like ;
coherence
( meet (the_Target_of S) is Function-like & meet (the_Target_of S) is Relation-like ) ;
end;

registration
let S be GraphMeetSet;
cluster meet (the_Source_of S) -> meet (the_Edges_of S) -defined meet (the_Vertices_of S) -valued ;
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;
cluster meet (the_Target_of S) -> meet (the_Edges_of S) -defined meet (the_Vertices_of S) -valued ;
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;
end;

registration
let S be GraphMeetSet;
cluster meet (the_Source_of S) -> total ;
coherence
meet (the_Source_of S) is total
proof end;
cluster meet (the_Target_of S) -> total ;
coherence
meet (the_Target_of S) is total
proof end;
end;

:: a.k.a. Graph Intersection, but not to be confused with Intersection Graph
definition
let S be GraphMeetSet;
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
ex b1 being _Graph st
( the_Vertices_of b1 = meet (the_Vertices_of S) & the_Edges_of b1 = meet (the_Edges_of S) & the_Source_of b1 = meet (the_Source_of S) & the_Target_of b1 = meet (the_Target_of S) )
proof end;
end;

:: deftheorem Def29 defines GraphMeet GLIB_014:def 29 :
for S being GraphMeetSet
for b2 being _Graph holds
( b2 is GraphMeet of S iff ( the_Vertices_of b2 = meet (the_Vertices_of S) & the_Edges_of b2 = meet (the_Edges_of S) & the_Source_of b2 = meet (the_Source_of S) & the_Target_of b2 = meet (the_Target_of S) ) );

:: 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;
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
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 )
proof end;

registration
let S be GraphMeetSet;
cluster Relation-like NAT -defined Function-like finite [Graph-like] plain for GraphMeet of S;
existence
ex b1 being GraphMeet of S st b1 is plain
proof end;
end;

theorem :: GLIB_014:39
for G, H being _Graph holds
( G is GraphMeet of {H} iff G == H )
proof end;

definition
let G1, G2 be _Graph;
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
( ( G1 tolerates G2 & the_Vertices_of G1 meets the_Vertices_of G2 implies ex b1 being Subgraph of G1 ex S being GraphMeetSet st
( S = {G1,G2} & b1 is GraphMeet of S ) ) & ( ( not G1 tolerates G2 or not the_Vertices_of G1 meets the_Vertices_of G2 ) implies ex b1 being Subgraph of G1 st b1 == G1 ) )
proof end;
consistency
for b1 being Subgraph of G1 holds verum ;
end;

:: deftheorem Def30 defines GraphMeet GLIB_014:def 30 :
for G1, G2 being _Graph
for b3 being Subgraph of G1 holds
( ( G1 tolerates G2 & the_Vertices_of G1 meets the_Vertices_of G2 implies ( b3 is GraphMeet of G1,G2 iff ex S being GraphMeetSet st
( S = {G1,G2} & b3 is GraphMeet of S ) ) ) & ( ( not G1 tolerates G2 or not the_Vertices_of G1 meets the_Vertices_of G2 ) implies ( b3 is GraphMeet of G1,G2 iff b3 == G1 ) ) );

:: not really needed
::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) ) )
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
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
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 )
proof end;

registration
let G1, G2 be _Graph;
cluster Relation-like NAT -defined Function-like finite [Graph-like] plain for GraphMeet of G1,G2;
existence
ex b1 being GraphMeet of G1,G2 st b1 is plain
proof end;
end;

theorem :: GLIB_014:44
for G, G1 being _Graph
for G2 being Subgraph of G1 holds
( G is GraphMeet of G1,G2 iff G == G2 )
proof 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
proof end;

registration
let G1 be _Graph;
let G2 be DLGraphComplement of G1;
cluster -> edgeless for GraphMeet of G1,G2;
coherence
for b1 being GraphMeet of G1,G2 holds b1 is edgeless
proof end;
end;

registration
let G1 be _Graph;
let G2 be LGraphComplement of G1;
cluster -> edgeless for GraphMeet of G1,G2;
coherence
for b1 being GraphMeet of G1,G2 holds b1 is edgeless
proof end;
end;

registration
let G1 be _Graph;
let G2 be DGraphComplement of G1;
cluster -> edgeless for GraphMeet of G1,G2;
coherence
for b1 being GraphMeet of G1,G2 holds b1 is edgeless
proof end;
end;

registration
let G1 be _Graph;
let G2 be GraphComplement of G1;
cluster -> edgeless for GraphMeet of G1,G2;
coherence
for b1 being GraphMeet of G1,G2 holds b1 is edgeless
proof end;
end;