let P, Q, R be PNPair; ( Q in compn P & R in untn P implies Q is_completion_of R )
assume that
A1:
Q in compn P
and
A2:
R in untn P
; Q is_completion_of R
consider Q1 being PNPair such that
A3:
Q1 = Q
and
A4:
Q1 in comp (untn P)
by A1;
A5:
ex R1 being PNPair st
( R1 = R & rng (R1 `1) = untn (rng (P `1)) & rng (R1 `2) = untn (rng (P `2)) )
by A2;
consider x being set such that
A6:
Q1 in x
and
A7:
x in { (comp S) where S is PNPair : S in untn P }
by A4, TARSKI:def 4;
consider S being PNPair such that
A8:
x = comp S
and
A9:
S in untn P
by A7;
consider Q2 being consistent PNPair such that
A10:
Q2 = Q1
and
A11:
Q2 is_completion_of S
by A6, A8;
A12:
ex S1 being PNPair st
( S1 = S & rng (S1 `1) = untn (rng (P `1)) & rng (S1 `2) = untn (rng (P `2)) )
by A9;
tau (rng S) = rng Q2
by A11;
then A13:
tau (rng R) = rng Q
by A3, A10, A12, A5;
( rng (R `1) c= rng (Q `1) & rng (R `2) c= rng (Q `2) )
by A11, A3, A10, A12, A5;
hence
Q is_completion_of R
by A13; verum