let G be _Graph; :: thesis: for v being Vertex of G
for e being object st v is endvertex holds
not e Joins v,v,G
let v be Vertex of G; :: thesis: for e being object st v is endvertex holds
not e Joins v,v,G
let e be object ; :: thesis: ( v is endvertex implies not e Joins v,v,G )
assume v is endvertex ; :: thesis: not e Joins v,v,G
then consider e0 being object such that
A1: ( v .edgesInOut() = {e0} & not e0 Joins v,v,G ) ;
assume A2: e Joins v,v,G ; :: thesis: contradiction
then e in v .edgesInOut() by Th62;
hence contradiction by A1, A2, TARSKI:def 1; :: thesis: verum