---

{ [T:Type]
    g:LabeledGraph(T). a,b:lg-size(g).
      (lg-edge(g;a;b)  lg-connected(g;a;b)) }

{ Proof }

---

Definitions occuring in Statement :  lg-connected: lg-connected(g;a;b),  lg-edge: lg-edge(g;a;b),  lg-size: lg-size(g),  labeled-graph: LabeledGraph(T),  int_seg: {i..j},  uall: [x:A]. B[x],  all: x:A. B[x],  implies: P  Q,  natural_number: $n,  universe: Type
Definitions :  uall: [x:A]. B[x],  all: x:A. B[x],  implies: P  Q,  lg-connected: lg-connected(g;a;b),  member: t  T,  prop: ,  and: P  Q,  infix_ap: x f y,  exists: x:A. B[x],  nat: ,  uimplies: b supposing a,  iff: P  Q,  rev_implies: P  Q
Lemmas :  lg-edge_wf,  int_seg_wf,  lg-size_wf,  nat_wf,  labeled-graph_wf,  rel_star_weakening,  rel_star_wf,  rel_plus_iff

---

\mforall{}[T:Type].  \mforall{}g:LabeledGraph(T).  \mforall{}a,b:\mBbbN{}lg-size(g).    (lg-edge(g;a;b)  {}\mRightarrow{}  lg-connected(g;a;b))


Date html generated: 2011_08_16-PM-06_40_33
Last ObjectModification: 2011_06_20-AM-01_59_35

Home Index