let X be set ; :: thesis: for p, q being XFinSequence
for n being Element of NAT st Shift ((p ^ q),n) c= X holds
Shift (p,n) c= X
let p, q be XFinSequence; :: thesis: for n being Element of NAT st Shift ((p ^ q),n) c= X holds
Shift (p,n) c= X
let n be Element of NAT ; :: thesis: ( Shift ((p ^ q),n) c= X implies Shift (p,n) c= X )
assume A1: Shift ((p ^ q),n) c= X ; :: thesis: Shift (p,n) c= X
Shift (p,n) c= Shift ((p ^ q),n) by Th84;
hence Shift (p,n) c= X by A1, XBOOLE_1:1; :: thesis: verum