let
R
be non
empty
transitive
mediate
RelStr
;
:: thesis:
for
X
being
Subset
of
R
holds
UAp
X
=
UAp
(
UAp
X
)
let
X
be
Subset
of
R
;
:: thesis:
UAp
X
=
UAp
(
UAp
X
)
A0
:
UAp
X
c=
UAp
(
UAp
X
)
by
ROUGHS_2:39
;
UAp
(
UAp
X
)
c=
UAp
X
by
Th95H
;
hence
UAp
X
=
UAp
(
UAp
X
)
by
A0
,
XBOOLE_0:def 10
;
:: thesis:
verum