theorem
:: WAYBEL29:4
for
X
,
Y
being non
empty
set
for
Z
being non
empty
Poset
for
T
being non
empty
full
SubRelStr
of
Z
|^
[:
X
,
Y
:]
for
S
being non
empty
full
SubRelStr
of
(
Z
|^
Y
)
|^
X
for
f
being
Function
of
S
,
T
st
f
is
uncurrying
&
f
is
V7
() &
f
is
onto
holds
f
is
isomorphic