---

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

{ Proof }

---

Definitions occuring in Statement :  lg-connected: lg-connected(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),  infix_ap: x f y,  member: t  T,  nat: ,  prop: ,  trans: Trans(T;x,y.E[x; y])
Lemmas :  rel_plus_wf,  int_seg_wf,  lg-size_wf,  nat_wf,  lg-edge_wf,  labeled-graph_wf,  rel_plus_trans

---

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


Date html generated: 2011_08_16-PM-06_40_50
Last ObjectModification: 2011_06_20-AM-01_59_54

Home Index