reconsider
S
=
bool
X
as
semiring_of_sets
of
X
by
SRINGS_2:5
;
S
is
cap-closed
;
hence
ex
b
_{1}
being
semiring_of_sets
of
X
st
b
_{1}
is
cap-closed
;
:: thesis:
verum