Conclusion
1.
FORALL
e_4176:doubleton[T]
:
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_4176)
IMPLIES
(FORALL
x_4177:T
:
e_4176(x_4177)
IMPLIES
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_4177))
Tactic
SKOSIMP*
Premise 1. (has proof of 8 steps)
-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)
