let Omega be non empty set ; :: thesis: for x, y being Subset of Omega st x misses y holds
(x,y) followed_by ({} Omega) is V62()
let x, y be Subset of Omega; :: thesis: ( x misses y implies (x,y) followed_by ({} Omega) is V62() )
assume A1: x misses y ; :: thesis: (x,y) followed_by ({} Omega) is V62()
reconsider r = (x,y) followed_by ({} Omega) as sequence of (bool Omega) ;
now :: thesis: for n, m being Element of NAT st n < m holds
r . n misses r . m
let n, m be Element of NAT ; :: thesis: ( n < m implies r . n misses r . m )
A2: ( m > 1 implies r . m = {} ) by FUNCT_7:124;
assume A3: n < m ; :: thesis: r . n misses r . m
A4: now :: thesis: ( ( m = 0 or m = 1 ) implies ( n = 0 & m = 1 ) )
assume A5: ( m = 0 or m = 1 ) ; :: thesis: ( n = 0 & m = 1 )
0 + 1 = 1 ;
then n <= 0 by A3, A5, NAT_1:13;
hence ( n = 0 & m = 1 ) by A3, A5, NAT_1:3; :: thesis: verum
end;
r . 0 = x by FUNCT_7:122;
hence r . n misses r . m by A1, A4, A2, FUNCT_7:123, NAT_1:25, XBOOLE_1:65; :: thesis: verum
end;
hence (x,y) followed_by ({} Omega) is V62() ; :: thesis: verum