Conclusion
-1.
edges(G!1
WITH
[vert
:=
{i:T
|
vert(G!1)(i)
AND
V!1(i)},
edges
:=
{e:doubleton[T]
|
edges(G!1)(e)
AND
(FORALL
x:T
:
e(x)
IMPLIES
V!1(x))}])(e!1)
-2.
e!1(x!1)
1.
vert(G!1
WITH
[vert
:=
{i:T
|
vert(G!1)(i)
AND
V!1(i)},
edges
:=
{e:doubleton[T]
|
edges(G!1)(e)
AND
(FORALL
x:T
:
e(x)
IMPLIES
V!1(x))}])(x!1)