environ
vocabularies HIDDEN, STRUCT_0, ORDERS_2, RELAT_1, TARSKI, ZFMISC_1, CARD_3, RELAT_2, XBOOLE_0, PARTFUN1, SUBSET_1, FUNCT_1, EQREL_1, XXREAL_0, ROUGHS_1, ROUGHS_2, FINSET_1, ROUGHS_3, ROUGHS_4, COHSP_1, FUNCT_2, FINSUB_1, SETWISEO, ALTCAT_2, CLASSES1, NATTRA_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FINSET_1, FINSUB_1, SETWISEO, CLASSES1, FUNCT_1, RELSET_1, FUNCT_2, DOMAIN_1, STRUCT_0, ORDERS_2, EQREL_1, ORDERS_3, ROUGHS_1, ROUGHS_2, ALTCAT_2, COHSP_1, ROUGHS_4;
definitions TARSKI, XBOOLE_0, COHSP_1;
theorems XBOOLE_0, XBOOLE_1, SUBSET_1, TARSKI, ZFMISC_1, RELAT_1, RELAT_2, FUNCT_2, ORDERS_2, ROUGHS_1, RELSET_1, ROUGHS_2, XTUPLE_0, RELSET_2, ROUGHS_4, FINSUB_1, YELLOW_0, ALTCAT_2, COHSP_1, FUNCT_1, FINSET_1, CLASSES1, ORDERS_1, ORDERS_3;
schemes FINSET_1, RELSET_1, SETWISEO;
registrations XBOOLE_0, SUBSET_1, RELAT_1, STRUCT_0, ORDERS_2, RELSET_1, ROUGHS_1, ROUGHS_2, FINSET_1, ROUGHS_4, FUNCT_2, SETWISEO, COHSP_1, WAYBEL_8;
constructors HIDDEN, EQREL_1, DOMAIN_1, RELSET_1, ROUGHS_1, SETWISEO, COHSP_1, ORDERS_3, YELLOW_3, ROUGHS_2, ROUGHS_4, ALTCAT_2;
requirements HIDDEN, BOOLE, SUBSET;
equalities SUBSET_1, STRUCT_0, RELAT_1;
expansions ;
UApCon:
for R being non empty RelStr
for X, Y being Subset of R holds UAp (X /\ Y) c= (UAp X) /\ (UAp Y)
Prop17A:
for R1, R2 being non empty RelStr st the carrier of R1 = the carrier of R2 & UAp R1 cc= UAp R2 holds
the InternalRel of R1 c= the InternalRel of R2
Corr3A:
for R1, R2 being non empty RelStr st the carrier of R1 = the carrier of R2 & UAp R1 = UAp R2 holds
the InternalRel of R1 = the InternalRel of R2
Prop18:
for R1, R2 being non empty RelStr st the carrier of R1 = the carrier of R2 & LAp R1 cc= LAp R2 holds
the InternalRel of R2 c= the InternalRel of R1
The5:
for R1, R2 being non empty RelStr st the carrier of R1 = the carrier of R2 holds
( UAp R1 = UAp R2 iff the InternalRel of R1 = the InternalRel of R2 )