let V be non empty set ; for E being Relation of V holds VertexDomRel (createGraph (V,E)) = E
let E be Relation of V; VertexDomRel (createGraph (V,E)) = E
set G0 = createGraph (V,E);
now for v, w being object holds
( ( [v,w] in VertexDomRel (createGraph (V,E)) implies [v,w] in E ) & ( [v,w] in E implies [v,w] in VertexDomRel (createGraph (V,E)) ) )let v,
w be
object ;
( ( [v,w] in VertexDomRel (createGraph (V,E)) implies [v,w] in E ) & ( [v,w] in E implies [v,w] in VertexDomRel (createGraph (V,E)) ) )hereby ( [v,w] in E implies [v,w] in VertexDomRel (createGraph (V,E)) )
assume
[v,w] in VertexDomRel (createGraph (V,E))
;
[v,w] in Ethen consider e being
object such that A1:
e DJoins v,
w,
createGraph (
V,
E)
by Th1;
e in the_Edges_of (createGraph (V,E))
by A1, GLIB_000:def 14;
then A2:
e in E
;
then consider v0,
w0 being
object such that A3:
e = [v0,w0]
by RELAT_1:def 1;
e DJoins v0,
w0,
createGraph (
V,
E)
by A2, A3, Th63;
then
(
v0 = v &
w0 = w )
by A1, GLIB_009:6;
hence
[v,w] in E
by A2, A3;
verum
end; assume
[v,w] in E
;
[v,w] in VertexDomRel (createGraph (V,E))then
[v,w] DJoins v,
w,
createGraph (
V,
E)
by Th63;
hence
[v,w] in VertexDomRel (createGraph (V,E))
by Th1;
verum end;
hence
VertexDomRel (createGraph (V,E)) = E
by RELAT_1:def 2; verum