set R = pcs-general-power P,D;
set IR = the InternalRel of (pcs-general-power P,D);
let x, y, z be set ; RELAT_2:def 8,ORDERS_2:def 5 ( not x in the carrier of (pcs-general-power P,D) or not y in the carrier of (pcs-general-power P,D) or not z in the carrier of (pcs-general-power P,D) or not [^,^] in the InternalRel of (pcs-general-power P,D) or not [^,^] in the InternalRel of (pcs-general-power P,D) or [^,^] in the InternalRel of (pcs-general-power P,D) )
assume that
A1:
x in the carrier of (pcs-general-power P,D)
and
y in the carrier of (pcs-general-power P,D)
and
A2:
z in the carrier of (pcs-general-power P,D)
and
A3:
[x,y] in the InternalRel of (pcs-general-power P,D)
and
A4:
[y,z] in the InternalRel of (pcs-general-power P,D)
; [^,^] in the InternalRel of (pcs-general-power P,D)
for a being set st a in x holds
ex b being set st
( b in z & [a,b] in the InternalRel of P )
proof
let a be
set ;
( a in x implies ex b being set st
( b in z & [a,b] in the InternalRel of P ) )
assume
a in x
;
ex b being set st
( b in z & [a,b] in the InternalRel of P )
then consider b being
set such that A5:
b in y
and A6:
[a,b] in the
InternalRel of
P
by A3, Def45;
consider c being
set such that A7:
c in z
and A8:
[b,c] in the
InternalRel of
P
by A4, A5, Def45;
take
c
;
( c in z & [a,c] in the InternalRel of P )
thus
c in z
by A7;
[a,c] in the InternalRel of P
A9:
the
InternalRel of
P is_transitive_in the
carrier of
P
by ORDERS_2:def 5;
A10:
a in the
carrier of
P
by A6, ZFMISC_1:106;
A11:
b in the
carrier of
P
by A6, ZFMISC_1:106;
c in the
carrier of
P
by A8, ZFMISC_1:106;
hence
[a,c] in the
InternalRel of
P
by A6, A8, A9, A10, A11, RELAT_2:def 8;
verum
end;
hence
[^,^] in the InternalRel of (pcs-general-power P,D)
by A1, A2, Def45; verum