let P be transitive pcs-Str ; for a being set st not a in the carrier of P holds
pcs-extension (P,a) is transitive
let a be set ; ( not a in the carrier of P implies pcs-extension (P,a) is transitive )
assume A1:
not a in the carrier of P
; pcs-extension (P,a) is transitive
set R = pcs-extension (P,a);
A2:
the InternalRel of (pcs-extension (P,a)) = [:{a}, the carrier of (pcs-extension (P,a)):] \/ the InternalRel of P
by Def39;
let x, y, z be object ; RELAT_2:def 8,ORDERS_2:def 3 ( not x in the carrier of (pcs-extension (P,a)) or not y in the carrier of (pcs-extension (P,a)) or not z in the carrier of (pcs-extension (P,a)) or not [^,^] in the InternalRel of (pcs-extension (P,a)) or not [^,^] in the InternalRel of (pcs-extension (P,a)) or [^,^] in the InternalRel of (pcs-extension (P,a)) )
assume that
A3:
x in the carrier of (pcs-extension (P,a))
and
A4:
y in the carrier of (pcs-extension (P,a))
and
A5:
z in the carrier of (pcs-extension (P,a))
and
A6:
[x,y] in the InternalRel of (pcs-extension (P,a))
and
A7:
[y,z] in the InternalRel of (pcs-extension (P,a))
; [^,^] in the InternalRel of (pcs-extension (P,a))
A8:
[a,z] in [:{a}, the carrier of (pcs-extension (P,a)):]
by A5, ZFMISC_1:105;
reconsider x = x, y = y, z = z as Element of (pcs-extension (P,a)) by A3, A4, A5;
A9:
x <= y
by A6;
A10:
y <= z
by A7;
per cases
( x = a or x <> a )
;
suppose A11:
x <> a
;
[^,^] in the InternalRel of (pcs-extension (P,a))then reconsider x0 =
x as
Element of
P by Th25;
A12:
x0 <> a
by A11;
then reconsider y0 =
y as
Element of
P by A1, A9, Th24;
y0 <> a
by A1, A9, A12, Th24;
then reconsider z0 =
z as
Element of
P by A1, A10, Th24;
A13:
y <> a
by A1, A9, A12, Th24;
A14:
x0 <= y0
by A9, A11, Th26;
y0 <= z0
by A10, A13, Th26;
then
x0 <= z0
by A14, YELLOW_0:def 2;
then
x <= z
by Th23;
hence
[^,^] in the
InternalRel of
(pcs-extension (P,a))
;
verum end;