environ
vocabularies HIDDEN, SUBSET_1, XBOOLE_0, TARSKI, ZFMISC_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1;
definitions ;
theorems TARSKI, SUBSET_1, ZFMISC_1;
schemes ;
registrations SUBSET_1;
constructors HIDDEN, TARSKI, SUBSET_1;
requirements HIDDEN, BOOLE;
equalities ;
expansions ;
theorem Th3:
for
a,
b being
set holds
(
a is
Subset of
b iff
a c= b )
:: "requirements SUBSET" is included in the environment description
:: of an article. They are published for testing purposes only.
:: Users should use appropriate requirements instead of referencing
:: to these theorems.
:: Some of these items need also "requirements BOOLE" for proper work.