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 set ; RELAT_2:def 8,ORDERS_2:def 5 ( 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:128;
reconsider x = x, y = y, z = z as Element of (pcs-extension P,a) by A3, A4, A5;
A9:
x <= y
by A6, ORDERS_2:def 9;
A10:
y <= z
by A7, ORDERS_2:def 9;
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)
by ORDERS_2:def 9;
verum end;