let P be pcs-Str ; :: thesis: for a being set
for p being Element of (pcs-extension (P,a)) st p <> a holds
p in the carrier of P
let a be set ; :: thesis: for p being Element of (pcs-extension (P,a)) st p <> a holds
p in the carrier of P
let p be Element of (pcs-extension (P,a)); :: thesis: ( p <> a implies p in the carrier of P )
assume A1: p <> a ; :: thesis: p in the carrier of P
the carrier of (pcs-extension (P,a)) = {a} \/ the carrier of P by Def39;
then ( p in {a} or p in the carrier of P ) by XBOOLE_0:def 3;
hence p in the carrier of P by A1, TARSKI:def 1; :: thesis: verum