let P, Q, R be PNPair; :: thesis: for T being pnptree of P st R in rng T & Q in untn R holds
comp Q c= rngr T
let T be pnptree of P; :: thesis: ( R in rng T & Q in untn R implies comp Q c= rngr T )
assume that
A1: R in rng T and
A2: Q in untn R ; :: thesis: comp Q c= rngr T
let S be object ; :: according to TARSKI:def 3 :: thesis: ( not S in comp Q or S in rngr T )
assume A3: S in comp Q ; :: thesis: S in rngr T
comp Q c= comp (untn R) by Th14, A2;
then A4: S in compn R by A3;
consider t being object such that
A5: t in dom T and
A6: T . t = R by FUNCT_1:def 3, A1;
reconsider t = t as Element of dom T by A5;
succ (T,t) = the Enumeration of compn R by Def11, A6;
then S in rng (succ (T,t)) by RLAFFIN3:def 1, A4;
then consider t1 being Element of dom T such that
A7: S = T . t1 and
A8: t1 in succ t by TREES_9:42;
ex n being Nat st
( t1 = t ^ <*n*> & t ^ <*n*> in dom T ) by A8;
hence S in rngr T by A7; :: thesis: verum