let P, Q, R be PNPair; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum