let
R
be non
empty
finite
negative_alliance
RelStr
;
:: thesis:
for
X
being
Subset
of
R
holds
(
LAp
X
)
`
c=
LAp
(
(
LAp
X
)
`
)
for
X
being
Subset
of
R
holds
UAp
(
(
UAp
X
)
`
)
c=
(
UAp
X
)
`
by
Prop13H
;
hence
for
X
being
Subset
of
R
holds
(
LAp
X
)
`
c=
LAp
(
(
LAp
X
)
`
)
by
Conv
;
:: thesis:
verum