let
X
,
Y
be
set
;
:: thesis:
for
R
being
Relation
holds
(
R
|_2
X
)
|_2
Y
=
R
|_2
(
X
/\
Y
)
let
R
be
Relation
;
:: thesis:
(
R
|_2
X
)
|_2
Y
=
R
|_2
(
X
/\
Y
)
thus
(
R
|_2
X
)
|_2
Y
=
R
/\
(
[:
X
,
X
:]
/\
[:
Y
,
Y
:]
)
by
XBOOLE_1:16
.=
R
|_2
(
X
/\
Y
)
by
ZFMISC_1:100
;
:: thesis:
verum