theorem Th30: :: PCS_0:30

for P being transitive pcs-Str
for a being set st not a in the carrier of P holds
pcs-extension (P,a) is transitive