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)))
AND
subgraph?(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))}],
G!1)
Tactic
PROP
Premise 1. (has proof of 9 steps)
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))
Premise 2. (has proof of 4 steps)
1.
subgraph?(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))}],
G!1)
