let n, m be Element of NAT ; :: thesis: for S being set
for Y being Subset of S
for F being Matrix of n,m,(bool S) st ex i, j being Element of NAT st
( i in Seg n & j in Seg m & F * (i,j) c= Y ) & ( for i1, j1, i2, j2 being Element of NAT st i1 in Seg n & i2 in Seg n & j1 in Seg m & j2 in Seg m & i1,j1,i2,j2 are_adjacent holds
( F * (i1,j1) c= Y iff F * (i2,j2) c= Y ) ) holds
for i, j being Element of NAT st i in Seg n & j in Seg m holds
F * (i,j) c= Y

let S be set ; :: thesis: for Y being Subset of S
for F being Matrix of n,m,(bool S) st ex i, j being Element of NAT st
( i in Seg n & j in Seg m & F * (i,j) c= Y ) & ( for i1, j1, i2, j2 being Element of NAT st i1 in Seg n & i2 in Seg n & j1 in Seg m & j2 in Seg m & i1,j1,i2,j2 are_adjacent holds
( F * (i1,j1) c= Y iff F * (i2,j2) c= Y ) ) holds
for i, j being Element of NAT st i in Seg n & j in Seg m holds
F * (i,j) c= Y

let Y be Subset of S; :: thesis: for F being Matrix of n,m,(bool S) st ex i, j being Element of NAT st
( i in Seg n & j in Seg m & F * (i,j) c= Y ) & ( for i1, j1, i2, j2 being Element of NAT st i1 in Seg n & i2 in Seg n & j1 in Seg m & j2 in Seg m & i1,j1,i2,j2 are_adjacent holds
( F * (i1,j1) c= Y iff F * (i2,j2) c= Y ) ) holds
for i, j being Element of NAT st i in Seg n & j in Seg m holds
F * (i,j) c= Y

let F be Matrix of n,m,(bool S); :: thesis: ( ex i, j being Element of NAT st
( i in Seg n & j in Seg m & F * (i,j) c= Y ) & ( for i1, j1, i2, j2 being Element of NAT st i1 in Seg n & i2 in Seg n & j1 in Seg m & j2 in Seg m & i1,j1,i2,j2 are_adjacent holds
( F * (i1,j1) c= Y iff F * (i2,j2) c= Y ) ) implies for i, j being Element of NAT st i in Seg n & j in Seg m holds
F * (i,j) c= Y )

assume that
A1: ex i, j being Element of NAT st
( i in Seg n & j in Seg m & F * (i,j) c= Y ) and
A2: for i1, j1, i2, j2 being Element of NAT st i1 in Seg n & i2 in Seg n & j1 in Seg m & j2 in Seg m & i1,j1,i2,j2 are_adjacent holds
( F * (i1,j1) c= Y iff F * (i2,j2) c= Y ) ; :: thesis: for i, j being Element of NAT st i in Seg n & j in Seg m holds
F * (i,j) c= Y

consider i1, j1 being Element of NAT such that
A3: i1 in Seg n and
A4: j1 in Seg m and
A5: F * (i1,j1) c= Y by A1;
A6: j1 <= m by ;
1 <= i1 by ;
then i1 - 1 >= 1 - 1 by XREAL_1:9;
then A7: i1 -' 1 = i1 - 1 by XREAL_0:def 2;
1 <= j1 by ;
then j1 - 1 >= 1 - 1 by XREAL_1:9;
then A8: j1 -' 1 = j1 - 1 by XREAL_0:def 2;
A9: i1 <= n by ;
thus for i, j being Element of NAT st i in Seg n & j in Seg m holds
F * (i,j) c= Y :: thesis: verum
proof
let i2, j2 be Element of NAT ; :: thesis: ( i2 in Seg n & j2 in Seg m implies F * (i2,j2) c= Y )
assume that
A10: i2 in Seg n and
A11: j2 in Seg m ; :: thesis: F * (i2,j2) c= Y
A12: j2 <= m by ;
1 <= i2 by ;
then i2 - 1 >= 1 - 1 by XREAL_1:9;
then A13: i2 -' 1 = i2 - 1 by XREAL_0:def 2;
1 <= j2 by ;
then j2 - 1 >= 1 - 1 by XREAL_1:9;
then A14: j2 -' 1 = j2 - 1 by XREAL_0:def 2;
A15: i2 <= n by ;
now :: thesis: ( ( ( n = 0 or m = 0 ) & contradiction ) or ( n <> 0 & m <> 0 & F * (i2,j2) c= Y ) )
per cases ( n = 0 or m = 0 or ( n <> 0 & m <> 0 ) ) ;
case ( n = 0 or m = 0 ) ; :: thesis: contradiction
end;
case A16: ( n <> 0 & m <> 0 ) ; :: thesis: F * (i2,j2) c= Y
then m >= 0 + 1 by NAT_1:13;
then m - 1 >= 0 by XREAL_1:19;
then A17: m -' 1 = m - 1 by XREAL_0:def 2;
then A18: ( j1 -' 1 <= m -' 1 & j2 -' 1 <= m -' 1 ) by ;
n >= 0 + 1 by ;
then n - 1 >= 0 by XREAL_1:19;
then A19: n -' 1 = n - 1 by XREAL_0:def 2;
then ( i1 -' 1 <= n -' 1 & i2 -' 1 <= n -' 1 ) by ;
then consider fs1, fs2 being FinSequence of NAT such that
A20: for i, k1, k2 being Element of NAT st i in dom fs1 & k1 = fs1 . i & k2 = fs2 . i holds
( k1 <= n -' 1 & k2 <= m -' 1 ) and
A21: fs1 . 1 = i1 -' 1 and
A22: fs1 . (len fs1) = i2 -' 1 and
A23: fs2 . 1 = j1 -' 1 and
A24: fs2 . (len fs2) = j2 -' 1 and
A25: len fs1 = len fs2 and
A26: len fs1 = (((((i1 -' 1) -' (i2 -' 1)) + ((i2 -' 1) -' (i1 -' 1))) + ((j1 -' 1) -' (j2 -' 1))) + ((j2 -' 1) -' (j1 -' 1))) + 1 and
A27: for i being Element of NAT st 1 <= i & i < len fs1 holds
fs1 /. i,fs2 /. i,fs1 /. (i + 1),fs2 /. (i + 1) are_adjacent by ;
deffunc H1( Nat) -> Element of NAT = (fs1 /. \$1) + 1;
ex p being FinSequence of NAT st
( len p = len fs1 & ( for j being Nat st j in dom p holds
p . j = H1(j) ) ) from then consider p1 being FinSequence of NAT such that
A28: len p1 = len fs1 and
A29: for k being Nat st k in dom p1 holds
p1 . k = (fs1 /. k) + 1 ;
deffunc H2( Nat) -> Element of NAT = (fs2 /. \$1) + 1;
ex p being FinSequence of NAT st
( len p = len fs2 & ( for k being Nat st k in dom p holds
p . k = H2(k) ) ) from then consider p2 being FinSequence of NAT such that
A30: len p2 = len fs2 and
A31: for k being Nat st k in dom p2 holds
p2 . k = (fs2 /. k) + 1 ;
A32: dom p2 = Seg (len fs2) by ;
defpred S1[ Nat] means ( \$1 + 1 <= len p1 implies F * ((p1 /. (\$1 + 1)),(p2 /. (\$1 + 1))) c= Y );
A33: dom p1 = Seg (len fs1) by ;
A34: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
A35: 1 <= k + 1 by NAT_1:12;
assume A36: ( k + 1 <= len p1 implies F * ((p1 /. (k + 1)),(p2 /. (k + 1))) c= Y ) ; :: thesis: S1[k + 1]
now :: thesis: ( ( k + 1 <= len p1 & S1[k + 1] ) or ( k + 1 > len p1 & S1[k + 1] ) )
per cases ( k + 1 <= len p1 or k + 1 > len p1 ) ;
case A37: k + 1 <= len p1 ; :: thesis: S1[k + 1]
now :: thesis: ( ( (k + 1) + 1 <= len p1 & S1[k + 1] ) or ( (k + 1) + 1 > len p1 & S1[k + 1] ) )
per cases ) + 1 <= len p1 or (k + 1) + 1 > len p1 ) ;
case A38: (k + 1) + 1 <= len p1 ; :: thesis: S1[k + 1]
set lp11 = fs1 /. ((k + 1) + 1);
set lp21 = fs2 /. ((k + 1) + 1);
1 <= (k + 1) + 1 by NAT_1:12;
then A39: (k + 1) + 1 in Seg (len p1) by ;
then (k + 1) + 1 in dom fs2 by ;
then A40: fs2 /. ((k + 1) + 1) = fs2 . ((k + 1) + 1) by PARTFUN1:def 6;
A41: (k + 1) + 1 in dom fs1 by ;
then A42: fs1 /. ((k + 1) + 1) = fs1 . ((k + 1) + 1) by PARTFUN1:def 6;
then fs1 /. ((k + 1) + 1) <= n - 1 by A19, A20, A41, A40;
then A43: (fs1 /. ((k + 1) + 1)) + 1 <= (n - 1) + 1 by XREAL_1:6;
(k + 1) + 1 in dom p2 by ;
then p2 . ((k + 1) + 1) = p2 /. ((k + 1) + 1) by PARTFUN1:def 6;
then A44: p2 /. ((k + 1) + 1) = (fs2 /. ((k + 1) + 1)) + 1 by A25, A28, A31, A32, A39;
fs2 /. ((k + 1) + 1) <= m -' 1 by A20, A41, A42, A40;
then A45: (fs2 /. ((k + 1) + 1)) + 1 <= (m - 1) + 1 by ;
1 <= 1 + (fs2 /. ((k + 1) + 1)) by NAT_1:11;
then A46: p2 /. ((k + 1) + 1) in Seg m by ;
(k + 1) + 1 in dom p1 by ;
then A47: p1 /. ((k + 1) + 1) = p1 . ((k + 1) + 1) by PARTFUN1:def 6
.= (fs1 /. ((k + 1) + 1)) + 1 by A28, A29, A33, A39 ;
set lp1 = fs1 /. (k + 1);
set lp2 = fs2 /. (k + 1);
A48: k + 1 < len p1 by ;
then A49: k + 1 in Seg (len p1) by ;
then k + 1 in dom fs2 by ;
then A50: fs2 /. (k + 1) = fs2 . (k + 1) by PARTFUN1:def 6;
k + 1 in dom p1 by ;
then A51: p1 /. (k + 1) = p1 . (k + 1) by PARTFUN1:def 6
.= (fs1 /. (k + 1)) + 1 by A28, A29, A33, A49 ;
A52: k + 1 in dom fs1 by ;
then A53: fs1 /. (k + 1) = fs1 . (k + 1) by PARTFUN1:def 6;
then fs1 /. (k + 1) <= n - 1 by A19, A20, A52, A50;
then A54: (fs1 /. (k + 1)) + 1 <= (n - 1) + 1 by XREAL_1:6;
1 <= 1 + (fs1 /. (k + 1)) by NAT_1:11;
then A55: p1 /. (k + 1) in Seg n by ;
k + 1 in dom p2 by ;
then A56: p2 /. (k + 1) = p2 . (k + 1) by PARTFUN1:def 6
.= (fs2 /. (k + 1)) + 1 by A25, A28, A31, A32, A49 ;
fs2 /. (k + 1) <= m -' 1 by A20, A52, A53, A50;
then A57: (fs2 /. (k + 1)) + 1 <= (m - 1) + 1 by ;
1 <= 1 + (fs2 /. (k + 1)) by NAT_1:11;
then A58: p2 /. (k + 1) in Seg m by ;
1 <= 1 + (fs1 /. ((k + 1) + 1)) by NAT_1:11;
then A59: p1 /. ((k + 1) + 1) in Seg n by ;
(k + 1) + 1 in dom p2 by ;
then p2 /. ((k + 1) + 1) = p2 . ((k + 1) + 1) by PARTFUN1:def 6
.= (fs2 /. ((k + 1) + 1)) + 1 by A25, A28, A31, A32, A39 ;
then p1 /. (k + 1),p2 /. (k + 1),p1 /. ((k + 1) + 1),p2 /. ((k + 1) + 1) are_adjacent by A27, A28, A35, A48, A51, A56, A47, Th3;
hence S1[k + 1] by A2, A36, A37, A55, A58, A59, A46; :: thesis: verum
end;
case (k + 1) + 1 > len p1 ; :: thesis: S1[k + 1]
hence S1[k + 1] ; :: thesis: verum
end;
end;
end;
hence S1[k + 1] ; :: thesis: verum
end;
case k + 1 > len p1 ; :: thesis: S1[k + 1]
hence S1[k + 1] by NAT_1:13; :: thesis: verum
end;
end;
end;
hence S1[k + 1] ; :: thesis: verum
end;
A60: 1 <= len fs1 by ;
then A61: 1 in Seg (len fs1) by FINSEQ_1:1;
then 1 in dom fs2 by ;
then A62: fs2 /. 1 = j1 -' 1 by ;
1 in dom p2 by ;
then A63: p2 /. 1 = p2 . 1 by PARTFUN1:def 6
.= (j1 -' 1) + 1 by A25, A31, A32, A61, A62
.= j1 by A8 ;
1 in dom fs1 by ;
then A64: fs1 /. 1 = i1 -' 1 by ;
1 in dom p1 by ;
then p1 /. 1 = p1 . 1 by PARTFUN1:def 6
.= (i1 -' 1) + 1 by A29, A33, A61, A64
.= i1 by A7 ;
then A65: S1[ 0 ] by ;
A66: for i being Nat holds S1[i] from 1 - 1 <= (len fs1) - 1 by ;
then (len fs1) -' 1 = (len fs1) - 1 by XREAL_0:def 2;
then A67: ((len fs1) -' 1) + 1 = len fs1 ;
A68: len fs1 in Seg (len fs1) by ;
then len fs1 in dom fs2 by ;
then A69: fs2 /. (len fs1) = j2 -' 1 by ;
len fs1 in dom p1 by ;
then A70: p1 /. (len fs1) = p1 . (len fs1) by PARTFUN1:def 6
.= (fs1 /. (len fs1)) + 1 by ;
len fs1 in dom fs1 by ;
then A71: fs1 /. (len fs1) = i2 -' 1 by ;
len fs1 in dom p2 by ;
then p2 /. (len fs1) = p2 . (len fs1) by PARTFUN1:def 6
.= (fs2 /. (len fs1)) + 1 by A25, A31, A32, A68 ;
hence F * (i2,j2) c= Y by A13, A14, A28, A66, A67, A70, A71, A69; :: thesis: verum
end;
end;
end;
hence F * (i2,j2) c= Y ; :: thesis: verum
end;