environ
vocabularies HIDDEN, XBOOLE_0, SUBSET_1, TARSKI, LATTICES, STRUCT_0, ALGSTR_0, EQREL_1, PBOOLE, LATTICE3, BINOP_1, FUNCT_1, WAYBEL_0, FINSET_1, RELAT_1, VECTSP_1, FINSEQ_1, GROUP_1, REWRITE1, SETWISEO, ZFMISC_1, SEQM_3, GRAPH_1, FUNCT_3, SETFAM_1, QUANTAL1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, FUNCT_1, RELSET_1, SETWISEO, PARTFUN1, FUNCT_2, BINOP_1, STRUCT_0, ALGSTR_0, FINSET_1, DOMAIN_1, LATTICES, LATTICE3, MONOID_0;
definitions TARSKI, BINOP_1, SETWISEO, LATTICES, LATTICE3, MONOID_0, STRUCT_0, XBOOLE_0;
theorems TARSKI, ZFMISC_1, BINOP_1, LATTICES, LATTICE3, SETWISEO, MONOID_0, FUNCT_1, FUNCT_2, RELSET_1, XBOOLE_1, GROUP_1;
schemes FUNCT_2, FRAENKEL;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FINSET_1, STRUCT_0, LATTICES, LATTICE3, ALGSTR_0, RELSET_1;
constructors HIDDEN, SETFAM_1, BINOP_1, DOMAIN_1, SETWISEO, VECTSP_1, LATTICE3, RELSET_1, GROUP_1;
requirements HIDDEN, BOOLE, SUBSET;
equalities LATTICES, ALGSTR_0;
expansions BINOP_1, SETWISEO, LATTICES;
deffunc H1( non empty LattStr ) -> set = the carrier of $1;
deffunc H2( LattStr ) -> Element of bool [:[: the carrier of $1, the carrier of $1:], the carrier of $1:] = the L_join of $1;
deffunc H3( LattStr ) -> Element of bool [:[: the carrier of $1, the carrier of $1:], the carrier of $1:] = the L_meet of $1;
deffunc H4( multMagma ) -> Element of bool [:[: the carrier of $1, the carrier of $1:], the carrier of $1:] = the multF of $1;
Lm1:
for A being non empty set
for f being UnOp of A st f is idempotent holds
for a being Element of A holds f . (f . a) = f . a
by FUNCT_2:15;