let V be non empty set ; for E being Relation of V
for v, w being object holds
( [v,w] in E iff [v,w] DJoins v,w, createGraph (V,E) )
let E be Relation of V; for v, w being object holds
( [v,w] in E iff [v,w] DJoins v,w, createGraph (V,E) )
let v, w be object ; ( [v,w] in E iff [v,w] DJoins v,w, createGraph (V,E) )
set G0 = createGraph (V,E);
hereby ( [v,w] DJoins v,w, createGraph (V,E) implies [v,w] in E )
assume A1:
[v,w] in E
;
[v,w] DJoins v,w, createGraph (V,E)then A2:
[v,w] in the_Edges_of (createGraph (V,E))
;
A3:
(
v in V &
w in V )
by A1, ZFMISC_1:87;
A4:
(the_Source_of (createGraph (V,E))) . [v,w] =
((pr1 (V,V)) | E) . [v,w]
.=
(pr1 (V,V)) . [v,w]
by A1, FUNCT_1:49
.=
(pr1 (V,V)) . (
v,
w)
by BINOP_1:def 1
.=
v
by A3, FUNCT_3:def 4
;
(the_Target_of (createGraph (V,E))) . [v,w] =
((pr2 (V,V)) | E) . [v,w]
.=
(pr2 (V,V)) . [v,w]
by A1, FUNCT_1:49
.=
(pr2 (V,V)) . (
v,
w)
by BINOP_1:def 1
.=
w
by A3, FUNCT_3:def 5
;
hence
[v,w] DJoins v,
w,
createGraph (
V,
E)
by A2, A4, GLIB_000:def 14;
verum
end;
assume
[v,w] DJoins v,w, createGraph (V,E)
; [v,w] in E
then
[v,w] in the_Edges_of (createGraph (V,E))
by GLIB_000:def 14;
hence
[v,w] in E
; verum