let G be _Graph; :: thesis: for P being Path of G
for n, m being odd Element of NAT st n < m & m <= len P & ( n <> 1 or m <> len P ) holds
P .cut (n,m) is open
let P be Path of G; :: thesis: for n, m being odd Element of NAT st n < m & m <= len P & ( n <> 1 or m <> len P ) holds
P .cut (n,m) is open
let n, m be odd Element of NAT ; :: thesis: ( n < m & m <= len P & ( n <> 1 or m <> len P ) implies P .cut (n,m) is open )
assume A1: ( n < m & m <= len P & ( n <> 1 or m <> len P ) ) ; :: thesis: P .cut (n,m) is open
then A2: ( (P .cut (n,m)) .first() = P . n & (P .cut (n,m)) .last() = P . m ) by GLIB_001:37;
assume P .cut (n,m) is closed ; :: thesis: contradiction
then P . n = P . m by A2, GLIB_001:def 24;
hence contradiction by A1, GLIB_001:def 28; :: thesis: verum