let f be non constant standard special_circular_sequence; :: thesis: for i1, j1, i2, j2 being Element of NAT st i1 <= len (GoB f) & j1 <= width (GoB f) & i2 <= len (GoB f) & j2 <= width (GoB f) & i1,j1,i2,j2 are_adjacent2 holds
( Int (cell (GoB f),i1,j1) c= (LeftComp f) \/ (RightComp f) iff Int (cell (GoB f),i2,j2) c= (LeftComp f) \/ (RightComp f) )
let i1, j1, i2, j2 be Element of NAT ; :: thesis: ( i1 <= len (GoB f) & j1 <= width (GoB f) & i2 <= len (GoB f) & j2 <= width (GoB f) & i1,j1,i2,j2 are_adjacent2 implies ( Int (cell (GoB f),i1,j1) c= (LeftComp f) \/ (RightComp f) iff Int (cell (GoB f),i2,j2) c= (LeftComp f) \/ (RightComp f) ) )
assume that
A1: ( i1 <= len (GoB f) & j1 <= width (GoB f) ) and
A2: i2 <= len (GoB f) and
A3: j2 <= width (GoB f) and
A4: i1,j1,i2,j2 are_adjacent2 ; :: thesis: ( Int (cell (GoB f),i1,j1) c= (LeftComp f) \/ (RightComp f) iff Int (cell (GoB f),i2,j2) c= (LeftComp f) \/ (RightComp f) )
A5: ( ( i1,i2 are_adjacent1 & j1 = j2 ) or ( i1 = i2 & j1,j2 are_adjacent1 ) ) by A4, GOBRD10:def 2;

now

per cases ( ( ( i2 = i1 + 1 or i1 = i2 + 1 ) & j1 = j2 ) or ( i1 = i2 & ( j2 = j1 + 1 or j1 = j2 + 1 ) ) ) by A5, GOBRD10:def 1;

case ( ( i2 = i1 + 1 or i1 = i2 + 1 ) & j1 = j2 ) ; :: thesis: ( Int (cell (GoB f),i1,j1) c= (LeftComp f) \/ (RightComp f) iff Int (cell (GoB f),i2,j2) c= (LeftComp f) \/ (RightComp f) )

hence ( Int (cell (GoB f),i1,j1) c= (LeftComp f) \/ (RightComp f) iff Int (cell (GoB f),i2,j2) c= (LeftComp f) \/ (RightComp f) ) by A1, A2, Lm5; :: thesis: verum

end;

case ( i1 = i2 & ( j2 = j1 + 1 or j1 = j2 + 1 ) ) ; :: thesis: ( Int (cell (GoB f),i1,j1) c= (LeftComp f) \/ (RightComp f) iff Int (cell (GoB f),i2,j2) c= (LeftComp f) \/ (RightComp f) )

hence ( Int (cell (GoB f),i1,j1) c= (LeftComp f) \/ (RightComp f) iff Int (cell (GoB f),i2,j2) c= (LeftComp f) \/ (RightComp f) ) by A1, A3, Lm6; :: thesis: verum

end;

end;

end;

hence ( Int (cell (GoB f),i1,j1) c= (LeftComp f) \/ (RightComp f) iff Int (cell (GoB f),i2,j2) c= (LeftComp f) \/ (RightComp f) ) ; :: thesis: verum