environ
vocabularies HIDDEN, WAYBEL_0, WAYBEL11, WAYBEL_9, SUBSET_1, WAYBEL17, EQREL_1, ORDINAL2, FUNCT_1, STRUCT_0, TARSKI, YELLOW_1, XBOOLE_0, ORDERS_2, RELAT_2, SEQM_3, XXREAL_0, RELAT_1, FUNCOP_1, LATTICES, LATTICE3, NEWTON, REWRITE1, YELLOW_0, FUNCT_2, ZFMISC_1, BORSUK_1, FUNCT_5, MCART_1, PRE_TOPC, CAT_1, MONOID_0, WAYBEL_3, PBOOLE, CARD_3, FUNCT_4, WAYBEL24;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, FUNCT_2, BINOP_1, DOMAIN_1, FUNCT_5, MONOID_0, CARD_3, PBOOLE, FUNCOP_1, STRUCT_0, PRE_TOPC, ORDERS_2, LATTICE3, FUNCT_7, YELLOW_0, ORDERS_3, WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_3, WAYBEL_9, WAYBEL11, WAYBEL17, YELLOW_3;
definitions TARSKI, WAYBEL_0, LATTICE3, ORDERS_2, MONOID_0, XBOOLE_0;
theorems WAYBEL_0, TARSKI, FUNCT_1, FUNCT_2, YELLOW_0, YELLOW_2, WAYBEL_1, ZFMISC_1, WAYBEL10, WAYBEL17, YELLOW_3, MCART_1, FUNCT_5, YELLOW_5, YELLOW10, FUNCOP_1, YELLOW_1, WAYBEL_3, CARD_3, FUNCT_7, RELAT_1, WAYBEL15, RELSET_1, XBOOLE_0, XBOOLE_1, XTUPLE_0;
schemes XBOOLE_0;
registrations XBOOLE_0, SUBSET_1, RELSET_1, FUNCT_2, STRUCT_0, LATTICE3, YELLOW_0, MONOID_0, WAYBEL_0, YELLOW_1, YELLOW_3, WAYBEL_3, WAYBEL10, WAYBEL11, WAYBEL17, PRE_TOPC, RELAT_1;
constructors HIDDEN, FUNCT_7, BORSUK_1, MONOID_0, ORDERS_3, WAYBEL_1, WAYBEL_3, WAYBEL17, YELLOW_3, FUNCT_5;
requirements HIDDEN, SUBSET, BOOLE;
equalities WAYBEL_0, BINOP_1, STRUCT_0;
expansions TARSKI, WAYBEL_0, LATTICE3, ORDERS_2, MONOID_0, XBOOLE_0;
scheme
Fraenkel6A{
F1()
-> LATTICE,
F2(
set )
-> set ,
P1[
set ],
P2[
set ] } :
{ F2(v1) where v1 is Element of F1() : P1[v1] } = { F2(v2) where v2 is Element of F1() : P2[v2] }
provided
A1:
for
v being
Element of
F1() holds
(
P1[
v] iff
P2[
v] )
Lm1:
for S being non empty RelStr
for D being non empty Subset of S holds D = { i where i is Element of S : i in D }