environ
vocabularies HIDDEN, STRUCT_0, ORDERS_2, RELAT_1, TARSKI, ZFMISC_1, PRE_TOPC, RELAT_2, XBOOLE_0, PARTFUN1, SUBSET_1, TOPS_1, FUNCT_1, FINSET_1, EQREL_1, XXREAL_0, ROUGHS_1, RCOMP_1, ROUGHS_2;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FINSET_1, RELAT_1, RELAT_2, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, DOMAIN_1, STRUCT_0, ORDERS_2, EQREL_1, PRE_TOPC, TOPS_1, ROUGHS_1, YELLOW_3;
definitions TARSKI, XBOOLE_0, SUBSET_1, STRUCT_0, RELAT_1, FUNCT_2, ROUGHS_1;
theorems EQREL_1, XBOOLE_0, XBOOLE_1, SUBSET_1, TARSKI, ZFMISC_1, RELAT_1, RELAT_2, FUNCT_2, FUNCT_1, ORDERS_2, YELLOW_3, RELSET_1, PARTFUN1, XTUPLE_0, TDLAT_3, PRE_TOPC, TOPS_1;
schemes FUNCT_2, RELSET_1, CHAIN_1;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FINSET_1, NAT_1, STRUCT_0, ORDERS_2, RELSET_1, FUNCT_1, FUNCT_2, YELLOW_3, TOPS_1, PRE_TOPC;
constructors HIDDEN, EQREL_1, REALSET2, RELSET_1, ROUGHS_1, YELLOW_3, TOPS_1;
requirements HIDDEN, BOOLE, SUBSET, NUMERALS;
equalities TARSKI, XBOOLE_0, SUBSET_1, STRUCT_0, RELAT_1, FUNCT_2, ROUGHS_1;
expansions TARSKI, XBOOLE_0, SUBSET_1, STRUCT_0, RELAT_1, FUNCT_2, ROUGHS_1;
Lm1:
for R being RelStr st the InternalRel of R is_reflexive_in the carrier of R holds
R is serial
Lm2:
for R being non empty serial RelStr
for x being Element of R holds Class ( the InternalRel of R,x) <> {}