theorem LMStat2A: :: AESCIP_1:16

for i, j, i0, j0 being Nat st i in Seg 4 & j in Seg 4 & i0 in Seg 4 & j0 in Seg 4 & ( not i = i0 or not j = j0 ) holds
{ k where k is Nat : ( (1 + ((i -' 1) * 8)) + ((j -' 1) * 32) <= k & k <= (8 + ((i -' 1) * 8)) + ((j -' 1) * 32) ) } /\ { k where k is Nat : ( (1 + ((i0 -' 1) * 8)) + ((j0 -' 1) * 32) <= k & k <= (8 + ((i0 -' 1) * 8)) + ((j0 -' 1) * 32) ) } = {}