let x be Element of comp P; :: thesis: x is consistent
x in comp P ;
then ex Q being consistent PNPair st
( x = Q & Q is_completion_of P ) ;
hence x is consistent ; :: thesis: verum