A1: rng (e .--> v1) =
rng ({e} --> v1)
by FUNCOP_1:def 9
.=
{v1}
by FUNCOP_1:8
;
A2: rng (e .--> v2) =
rng ({e} --> v2)
by FUNCOP_1:def 9
.=
{v2}
by FUNCOP_1:8
;
A3: dom (e .--> v1) =
dom ({e} --> v1)
by FUNCOP_1:def 9
.=
{e}
;
A4: dom (e .--> v2) =
dom ({e} --> v2)
by FUNCOP_1:def 9
.=
{e}
;
hereby ( ( not v1 in the_Vertices_of G & v2 in the_Vertices_of G & not e in the_Edges_of G implies ex b1 being Supergraph of G st
( the_Vertices_of b1 = (the_Vertices_of G) \/ {v1} & the_Edges_of b1 = (the_Edges_of G) \/ {e} & the_Source_of b1 = (the_Source_of G) +* (e .--> v1) & the_Target_of b1 = (the_Target_of G) +* (e .--> v2) ) ) & ( ( not v1 in the_Vertices_of G or v2 in the_Vertices_of G or e in the_Edges_of G ) & ( v1 in the_Vertices_of G or not v2 in the_Vertices_of G or e in the_Edges_of G ) implies ex b1 being Supergraph of G st b1 == G ) )
assume A7:
(
v1 in the_Vertices_of G & not
v2 in the_Vertices_of G & not
e in the_Edges_of G )
;
ex G1 being Supergraph of G st
( the_Vertices_of G1 = (the_Vertices_of G) \/ {v2} & the_Edges_of G1 = (the_Edges_of G) \/ {e} & the_Source_of G1 = (the_Source_of G) +* (e .--> v1) & the_Target_of G1 = (the_Target_of G) +* (e .--> v2) )set V1 =
(the_Vertices_of G) \/ {v2};
reconsider V1 =
(the_Vertices_of G) \/ {v2} as non
empty set ;
set E1 =
(the_Edges_of G) \/ {e};
set S1 =
(the_Source_of G) +* (e .--> v1);
A8:
dom ((the_Source_of G) +* (e .--> v1)) =
(dom (the_Source_of G)) \/ (dom (e .--> v1))
by FUNCT_4:def 1
.=
(the_Edges_of G) \/ {e}
by FUNCT_2:def 1, A3
;
A9:
the_Vertices_of G c= V1
by XBOOLE_1:7;
(rng (the_Source_of G)) \/ {v1} c= (the_Vertices_of G) \/ {v1}
by XBOOLE_1:9;
then
(rng (the_Source_of G)) \/ {v1} c= the_Vertices_of G
by A7, ZFMISC_1:40;
then A10:
(rng (the_Source_of G)) \/ (rng (e .--> v1)) c= V1
by A1, A9, XBOOLE_1:1;
rng ((the_Source_of G) +* (e .--> v1)) c= (rng (the_Source_of G)) \/ (rng (e .--> v1))
by FUNCT_4:17;
then reconsider S1 =
(the_Source_of G) +* (e .--> v1) as
Function of
((the_Edges_of G) \/ {e}),
V1 by A8, A10, FUNCT_2:2, XBOOLE_1:1;
set T1 =
(the_Target_of G) +* (e .--> v2);
A11:
dom ((the_Target_of G) +* (e .--> v2)) =
(dom (the_Target_of G)) \/ (dom (e .--> v2))
by FUNCT_4:def 1
.=
(the_Edges_of G) \/ {e}
by FUNCT_2:def 1, A4
;
A12:
(rng (the_Target_of G)) \/ (rng (e .--> v2)) c= V1
by A2, XBOOLE_1:9;
rng ((the_Target_of G) +* (e .--> v2)) c= (rng (the_Target_of G)) \/ (rng (e .--> v2))
by FUNCT_4:17;
then reconsider T1 =
(the_Target_of G) +* (e .--> v2) as
Function of
((the_Edges_of G) \/ {e}),
V1 by A11, A12, FUNCT_2:2, XBOOLE_1:1;
set G1 =
createGraph (
V1,
((the_Edges_of G) \/ {e}),
S1,
T1);
the_Edges_of G c= (the_Edges_of G) \/ {e}
by XBOOLE_1:7;
then A13:
(
the_Edges_of G c= the_Edges_of (createGraph (V1,((the_Edges_of G) \/ {e}),S1,T1)) &
the_Vertices_of G c= the_Vertices_of (createGraph (V1,((the_Edges_of G) \/ {e}),S1,T1)) )
by A9;
for
e1 being
set st
e1 in the_Edges_of G holds
(
(the_Source_of G) . e1 = (the_Source_of (createGraph (V1,((the_Edges_of G) \/ {e}),S1,T1))) . e1 &
(the_Target_of G) . e1 = (the_Target_of (createGraph (V1,((the_Edges_of G) \/ {e}),S1,T1))) . e1 )
proof
let e1 be
set ;
( e1 in the_Edges_of G implies ( (the_Source_of G) . e1 = (the_Source_of (createGraph (V1,((the_Edges_of G) \/ {e}),S1,T1))) . e1 & (the_Target_of G) . e1 = (the_Target_of (createGraph (V1,((the_Edges_of G) \/ {e}),S1,T1))) . e1 ) )
assume
e1 in the_Edges_of G
;
( (the_Source_of G) . e1 = (the_Source_of (createGraph (V1,((the_Edges_of G) \/ {e}),S1,T1))) . e1 & (the_Target_of G) . e1 = (the_Target_of (createGraph (V1,((the_Edges_of G) \/ {e}),S1,T1))) . e1 )
then A14:
( not
e1 in dom (e .--> v1) & not
e1 in dom (e .--> v2) )
by A7, TARSKI:def 1;
thus (the_Source_of (createGraph (V1,((the_Edges_of G) \/ {e}),S1,T1))) . e1 =
((the_Source_of G) +* (e .--> v1)) . e1
.=
(the_Source_of G) . e1
by A14, FUNCT_4:11
;
(the_Target_of G) . e1 = (the_Target_of (createGraph (V1,((the_Edges_of G) \/ {e}),S1,T1))) . e1
thus (the_Target_of (createGraph (V1,((the_Edges_of G) \/ {e}),S1,T1))) . e1 =
((the_Target_of G) +* (e .--> v2)) . e1
.=
(the_Target_of G) . e1
by A14, FUNCT_4:11
;
verum
thus
verum
;
verum
end; then reconsider G1 =
createGraph (
V1,
((the_Edges_of G) \/ {e}),
S1,
T1) as
Supergraph of
G by A13, Def9;
take G1 =
G1;
( the_Vertices_of G1 = (the_Vertices_of G) \/ {v2} & the_Edges_of G1 = (the_Edges_of G) \/ {e} & the_Source_of G1 = (the_Source_of G) +* (e .--> v1) & the_Target_of G1 = (the_Target_of G) +* (e .--> v2) )thus
(
the_Vertices_of G1 = (the_Vertices_of G) \/ {v2} &
the_Edges_of G1 = (the_Edges_of G) \/ {e} &
the_Source_of G1 = (the_Source_of G) +* (e .--> v1) &
the_Target_of G1 = (the_Target_of G) +* (e .--> v2) )
;
verum
end;
hereby ( ( not v1 in the_Vertices_of G or v2 in the_Vertices_of G or e in the_Edges_of G ) & ( v1 in the_Vertices_of G or not v2 in the_Vertices_of G or e in the_Edges_of G ) implies ex b1 being Supergraph of G st b1 == G )
assume A15:
( not
v1 in the_Vertices_of G &
v2 in the_Vertices_of G & not
e in the_Edges_of G )
;
ex G1 being Supergraph of G st
( the_Vertices_of G1 = (the_Vertices_of G) \/ {v1} & the_Edges_of G1 = (the_Edges_of G) \/ {e} & the_Source_of G1 = (the_Source_of G) +* (e .--> v1) & the_Target_of G1 = (the_Target_of G) +* (e .--> v2) )set V1 =
(the_Vertices_of G) \/ {v1};
reconsider V1 =
(the_Vertices_of G) \/ {v1} as non
empty set ;
set E1 =
(the_Edges_of G) \/ {e};
set S1 =
(the_Source_of G) +* (e .--> v1);
A16:
dom ((the_Source_of G) +* (e .--> v1)) =
(dom (the_Source_of G)) \/ (dom (e .--> v1))
by FUNCT_4:def 1
.=
(the_Edges_of G) \/ {e}
by FUNCT_2:def 1, A3
;
A17:
the_Vertices_of G c= V1
by XBOOLE_1:7;
A18:
(rng (the_Source_of G)) \/ (rng (e .--> v1)) c= V1
by A1, XBOOLE_1:9;
rng ((the_Source_of G) +* (e .--> v1)) c= (rng (the_Source_of G)) \/ (rng (e .--> v1))
by FUNCT_4:17;
then reconsider S1 =
(the_Source_of G) +* (e .--> v1) as
Function of
((the_Edges_of G) \/ {e}),
V1 by A16, A18, FUNCT_2:2, XBOOLE_1:1;
set T1 =
(the_Target_of G) +* (e .--> v2);
A19:
dom ((the_Target_of G) +* (e .--> v2)) =
(dom (the_Target_of G)) \/ (dom (e .--> v2))
by FUNCT_4:def 1
.=
(the_Edges_of G) \/ {e}
by FUNCT_2:def 1, A4
;
(rng (the_Target_of G)) \/ {v2} c= (the_Vertices_of G) \/ {v2}
by XBOOLE_1:9;
then
(rng (the_Target_of G)) \/ {v2} c= the_Vertices_of G
by A15, ZFMISC_1:40;
then A20:
(rng (the_Target_of G)) \/ (rng (e .--> v2)) c= V1
by A2, A17, XBOOLE_1:1;
rng ((the_Target_of G) +* (e .--> v2)) c= (rng (the_Target_of G)) \/ (rng (e .--> v2))
by FUNCT_4:17;
then reconsider T1 =
(the_Target_of G) +* (e .--> v2) as
Function of
((the_Edges_of G) \/ {e}),
V1 by A19, A20, FUNCT_2:2, XBOOLE_1:1;
set G1 =
createGraph (
V1,
((the_Edges_of G) \/ {e}),
S1,
T1);
the_Edges_of G c= (the_Edges_of G) \/ {e}
by XBOOLE_1:7;
then A21:
(
the_Edges_of G c= the_Edges_of (createGraph (V1,((the_Edges_of G) \/ {e}),S1,T1)) &
the_Vertices_of G c= the_Vertices_of (createGraph (V1,((the_Edges_of G) \/ {e}),S1,T1)) )
by A17;
for
e1 being
set st
e1 in the_Edges_of G holds
(
(the_Source_of G) . e1 = (the_Source_of (createGraph (V1,((the_Edges_of G) \/ {e}),S1,T1))) . e1 &
(the_Target_of G) . e1 = (the_Target_of (createGraph (V1,((the_Edges_of G) \/ {e}),S1,T1))) . e1 )
proof
let e1 be
set ;
( e1 in the_Edges_of G implies ( (the_Source_of G) . e1 = (the_Source_of (createGraph (V1,((the_Edges_of G) \/ {e}),S1,T1))) . e1 & (the_Target_of G) . e1 = (the_Target_of (createGraph (V1,((the_Edges_of G) \/ {e}),S1,T1))) . e1 ) )
assume
e1 in the_Edges_of G
;
( (the_Source_of G) . e1 = (the_Source_of (createGraph (V1,((the_Edges_of G) \/ {e}),S1,T1))) . e1 & (the_Target_of G) . e1 = (the_Target_of (createGraph (V1,((the_Edges_of G) \/ {e}),S1,T1))) . e1 )
then A22:
( not
e1 in dom (e .--> v1) & not
e1 in dom (e .--> v2) )
by A15, TARSKI:def 1;
thus (the_Source_of (createGraph (V1,((the_Edges_of G) \/ {e}),S1,T1))) . e1 =
((the_Source_of G) +* (e .--> v1)) . e1
.=
(the_Source_of G) . e1
by A22, FUNCT_4:11
;
(the_Target_of G) . e1 = (the_Target_of (createGraph (V1,((the_Edges_of G) \/ {e}),S1,T1))) . e1
thus (the_Target_of (createGraph (V1,((the_Edges_of G) \/ {e}),S1,T1))) . e1 =
((the_Target_of G) +* (e .--> v2)) . e1
.=
(the_Target_of G) . e1
by A22, FUNCT_4:11
;
verum
thus
verum
;
verum
end; then reconsider G1 =
createGraph (
V1,
((the_Edges_of G) \/ {e}),
S1,
T1) as
Supergraph of
G by A21, Def9;
take G1 =
G1;
( the_Vertices_of G1 = (the_Vertices_of G) \/ {v1} & the_Edges_of G1 = (the_Edges_of G) \/ {e} & the_Source_of G1 = (the_Source_of G) +* (e .--> v1) & the_Target_of G1 = (the_Target_of G) +* (e .--> v2) )thus
(
the_Vertices_of G1 = (the_Vertices_of G) \/ {v1} &
the_Edges_of G1 = (the_Edges_of G) \/ {e} &
the_Source_of G1 = (the_Source_of G) +* (e .--> v1) &
the_Target_of G1 = (the_Target_of G) +* (e .--> v2) )
;
verum
end;
assume
( ( not v1 in the_Vertices_of G or v2 in the_Vertices_of G or e in the_Edges_of G ) & ( v1 in the_Vertices_of G or not v2 in the_Vertices_of G or e in the_Edges_of G ) )
; ex b1 being Supergraph of G st b1 == G
reconsider G1 = G as Supergraph of G by Th65;
take
G1
; G1 == G
thus
G1 == G
; verum