let T be non empty 1-sorted ; :: thesis: for S being sequence of T
for A, B being Subset of T st rng S c= A \/ B holds
ex S1 being subsequence of S st
( rng S1 c= A or rng S1 c= B )
let S be sequence of T; :: thesis: for A, B being Subset of T st rng S c= A \/ B holds
ex S1 being subsequence of S st
( rng S1 c= A or rng S1 c= B )
let A, B be Subset of T; :: thesis: ( rng S c= A \/ B implies ex S1 being subsequence of S st
( rng S1 c= A or rng S1 c= B ) )
assume A1: rng S c= A \/ B ; :: thesis: ex S1 being subsequence of S st
( rng S1 c= A or rng S1 c= B )
assume A2: for S1 being subsequence of S holds
( not rng S1 c= A & not rng S1 c= B ) ; :: thesis: contradiction
then consider n1 being Element of NAT such that
A3: for m being Element of NAT st n1 <= m holds
not S . m in A by Th3;
consider n2 being Element of NAT such that
A4: for m being Element of NAT st n2 <= m holds
not S . m in B by A2, Th3;
reconsider n = max (n1,n2) as Element of NAT ;
A5: not S . n in B by A4, XXREAL_0:25;
n in NAT ;
then n in dom S by NORMSP_1:12;
then A6: S . n in rng S by FUNCT_1:def 3;
not S . n in A by A3, XXREAL_0:25;
hence contradiction by A1, A5, A6, XBOOLE_0:def 3; :: thesis: verum