PVS: pf:subgraph_TCC1 - proof from subgraphs

FDL > PVS > Graphs > subgraphs > subgraph TCC1 > pf:subgraph TCC1 > 1 > 1 > 1 > 1 (3 nodes)

Conclusion

-1. subset?({e:doubleton[T] | edges(G!1)(e) AND (FORALL x:T : e(x) IMPLIES V!1(x))}, edges(G!1)) IMPLIES is finite({e:doubleton[T] | edges(G!1)(e) AND (FORALL x:T : e(x) IMPLIES V!1(x))})

1. is finite[doubleton[T]]({e:doubleton[T] | edges(G!1)(e) AND (FORALL x:T : e(x) IMPLIES V!1(x))})

Tactic
ASSERT

Premise 1. (has proof of 2 steps)

1. subset?({e:doubleton[T] | edges(G!1)(e) AND (FORALL x:T : e(x) IMPLIES V!1(x))}, edges(G!1))
2. is finite[doubleton[T]]({e:doubleton[T] | edges(G!1)(e) AND (FORALL x:T : e(x) IMPLIES V!1(x))})