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 that
A1: i in Seg (width G) and
A2: width G > 1 ; :: thesis: width G = (width (DelCol G,i)) + 1
ex m being Element of NAT st
( width G = m + 1 & m > 0 ) by A2, Th3;
hence width G = (width (DelCol G,i)) + 1 by A1, Th26; :: thesis: verum