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