reconsider n = (x .. p) - 1 as Element of NAT by A1, Th22;
reconsider q = p | (Seg n) as FinSequence by FINSEQ_1:15;
take q ; :: thesis: ex n being Nat st
( n = (x .. p) - 1 & q = p | (Seg n) )
thus ex n being Nat st
( n = (x .. p) - 1 & q = p | (Seg n) ) ; :: thesis: verum