reconsider Tt = T . t as Element of rng T by FUNCT_1:3;
Tt is consistent ;
hence for b₁ being PNPair st b₁ = T . t holds
( not b₁ is Inconsistent & b₁ is complete ) ; :: thesis: verum