let
X
be
set
;
:: thesis:
for
R
being
Relation
holds
R
_2
X
=
X
`
(
R

X
)
let
R
be
Relation
;
:: thesis:
R
_2
X
=
X
`
(
R

X
)
thus
R
_2
X
=
(
X
`
R
)

X
by
Th10
.=
X
`
(
R

X
)
by
RELAT_1:109
;
:: thesis:
verum