let X be set ; :: thesis: for S being SigmaField of X
for N, G, F being sequence of S st G . 0 = N . 0 & ( for n being Nat holds G . (n + 1) = (N . (n + 1)) \/ (G . n) ) & F . 0 = N . 0 & ( for n being Nat holds F . (n + 1) = (N . (n + 1)) \ (G . n) ) holds
for n, m being Nat st n < m holds
F . n misses F . m
let S be SigmaField of X; :: thesis: for N, G, F being sequence of S st G . 0 = N . 0 & ( for n being Nat holds G . (n + 1) = (N . (n + 1)) \/ (G . n) ) & F . 0 = N . 0 & ( for n being Nat holds F . (n + 1) = (N . (n + 1)) \ (G . n) ) holds
for n, m being Nat st n < m holds
F . n misses F . m
let N, G, F be sequence of S; :: thesis: ( G . 0 = N . 0 & ( for n being Nat holds G . (n + 1) = (N . (n + 1)) \/ (G . n) ) & F . 0 = N . 0 & ( for n being Nat holds F . (n + 1) = (N . (n + 1)) \ (G . n) ) implies for n, m being Nat st n < m holds
F . n misses F . m )
assume that
A1: ( G . 0 = N . 0 & ( for n being Nat holds G . (n + 1) = (N . (n + 1)) \/ (G . n) ) & F . 0 = N . 0 ) and
A2: for n being Nat holds F . (n + 1) = (N . (n + 1)) \ (G . n) ; :: thesis: for n, m being Nat st n < m holds
F . n misses F . m
let n, m be Nat; :: thesis: ( n < m implies F . n misses F . m )
assume A3: n < m ; :: thesis: F . n misses F . m
then 0 <> m by NAT_1:2;
then consider k being Nat such that
A4: m = k + 1 by NAT_1:6;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
F . (k + 1) = (N . (k + 1)) \ (G . k) by A2;
then A5: G . k misses F . (k + 1) by XBOOLE_1:79;
n <= k by A3, A4, NAT_1:13;
hence (F . n) /\ (F . m) = ((F . n) /\ (G . k)) /\ (F . (k + 1)) by A1, A2, A4, Th7, XBOOLE_1:28
.= (F . n) /\ ((G . k) /\ (F . (k + 1))) by XBOOLE_1:16
.= (F . n) /\ {} by A5
.= {} ;
:: according to XBOOLE_0:def 7 :: thesis: verum