let
X
,
Y
be
set
;
:: thesis:
for
R
being
Relation
holds
(
R
|_2
X
)
|_2
Y
=
(
R
|_2
Y
)
|_2
X
let
R
be
Relation
;
:: thesis:
(
R
|_2
X
)
|_2
Y
=
(
R
|_2
Y
)
|_2
X
thus
(
R
|_2
X
)
|_2
Y
=
R
|_2
(
Y
/\
X
)
by
Th19
.=
(
R
|_2
Y
)
|_2
X
by
Th19
;
:: thesis:
verum