set R = pcs-general-power (P,D);
set IR = the InternalRel of (pcs-general-power (P,D));
let x, y, z be object ; RELAT_2:def 8,ORDERS_2:def 3 ( 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))
reconsider x = x, y = y, z = z as set by TARSKI:1;
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 3;
A10:
a in the
carrier of
P
by A6, ZFMISC_1:87;
A11:
b in the
carrier of
P
by A6, ZFMISC_1:87;
c in the
carrier of
P
by A8, ZFMISC_1:87;
hence
[a,c] in the
InternalRel of
P
by A6, A8, A9, A10, A11;
verum
end;
hence
[^,^] in the InternalRel of (pcs-general-power (P,D))
by A1, A2, Def45; verum