let i be Element of NAT ; :: thesis: for G being Go-board st i in Seg (width G) & width G > 1 holds
width G = (width (DelCol G,i)) + 1
let G be Go-board; :: thesis: ( i in Seg (width G) & width G > 1 implies width G = (width (DelCol G,i)) + 1 )
assume A1: ( i in Seg (width G) & width G > 1 ) ; :: thesis: width G = (width (DelCol G,i)) + 1
then ex m being Element of NAT st
( width G = m + 1 & m > 0 ) by Th3;
hence width G = (width (DelCol G,i)) + 1 by A1, Th26; :: thesis: verum