environ
vocabularies HIDDEN, REALSET1, FINSEQ_1, GROUP_3, FUNCT_1, RLSUB_1, GROUP_2, RELAT_1, GROUP_6, XBOOLE_0, QC_LANG1, GROUP_1, GRAPH_1, ARYTM_1, ARYTM_3, ZFMISC_1, NUMBERS, SUBSET_1, XXREAL_1, STRUCT_0, NEWTON, TARSKI, NAT_1, PARTFUN1, PRE_TOPC, XXREAL_0, CARD_1, GROUP_4, NATTRA_1, CARD_3, BINOP_1, GROUP_5, GRSOLV_1, GRNILP_1, BCIALG_2, ALGSTR_0;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, XCMPLX_0, RELAT_1, FUNCT_1, RELSET_1, FUNCT_2, STRUCT_0, ALGSTR_0, PARTFUN1, FINSEQ_1, ZFMISC_1, ORDINAL1, XXREAL_0, NUMBERS, REALSET1, DOMAIN_1, GROUP_1, GROUP_3, GR_CY_1, GRSOLV_1, GROUP_4, GROUP_5, GROUP_2, GROUP_6;
definitions TARSKI, GRSOLV_1;
theorems FINSEQ_1, GROUP_2, GROUP_3, TARSKI, GROUP_5, GROUP_6, FINSEQ_2, FUNCT_2, RELAT_1, XBOOLE_0, XBOOLE_1, NAT_1, GROUP_1, PARTFUN1, FINSEQ_3, GROUP_4, FUNCT_1, GRSOLV_1, STRUCT_0, GROUP_11, XTUPLE_0;
schemes XBOOLE_0, FUNCT_1, FINSEQ_1, FINSEQ_2, XFAMILY;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, XREAL_0, INT_1, FINSEQ_1, STRUCT_0, GROUP_1, GROUP_2, GROUP_3, GROUP_6, GR_CY_1, ALGSTR_0, RELSET_1;
constructors HIDDEN, BINOP_1, BINARITH, GROUP_4, GROUP_5, GRSOLV_1, RELSET_1, GR_CY_1, REALSET1;
requirements HIDDEN, NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
equalities GROUP_2, GROUP_6, FINSEQ_1, GROUP_4, ALGSTR_0, GROUP_3, GROUP_5, GRSOLV_1, REALSET1;
expansions TARSKI;
Lm1:
for G being Group
for A being Subgroup of G holds gr (carr A) is Subgroup of A
Lm2:
for G being Group
for A being Subgroup of G holds A is Subgroup of (Omega). G
Lm3:
for G being Group
for H being Subgroup of G
for N being normal Subgroup of G holds [.N,H.] is Subgroup of N
Lm4:
for G being Group
for H being Subgroup of G holds ((Omega). G) /\ H = (Omega). H
Lm5:
for G being Group
for F1 being strict Subgroup of G
for H, F2 being Subgroup of G st F1 is normal Subgroup of F2 holds
F1 /\ H is normal Subgroup of F2 /\ H