:: GROUP_4 semantic presentation begin definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "D")); let "X" be ($#m1_hidden :::"set"::: ) ; :: original: :::"-"::: redefine func "F" :::"-"::: "X" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" "D"; end; scheme :: GROUP_4:sch 1 MeetSbgEx{ F1() -> ($#l3_algstr_0 :::"Group":::), P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "ex" (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set F1 "(" ")" ) "st" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set (Var "A")) where A "is" ($#m1_subset_1 :::"Subset":::) "of" (Set F1 "(" ")" ) : (Bool "ex" (Set (Var "K")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set F1 "(" ")" ) "st" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K")))) & (Bool P1[(Set (Var "K"))]) ")" )) "}" ))) provided (Bool "ex" (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set F1 "(" ")" ) "st" (Bool P1[(Set (Var "H"))])) proof end; scheme :: GROUP_4:sch 2 SubgrSep{ F1() -> ($#l3_algstr_0 :::"Group":::), P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "ex" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k1_group_3 :::"Subgroups"::: ) (Set F1 "(" ")" ))) & (Bool "(" "for" (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool "(" (Bool (Set (Var "H")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "iff" (Bool P1[(Set (Var "H"))]) ")" ) ")" ) ")" )) proof end; definitionlet "i" be ($#m1_hidden :::"Integer":::); func :::"@"::: "i" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) equals :: GROUP_4:def 1 "i"; end; :: deftheorem defines :::"@"::: GROUP_4:def 1 : (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set ($#k2_group_4 :::"@"::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Var "i")))); theorem :: GROUP_4:1 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "H")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "h")))) "holds" (Bool (Set (Set (Var "a")) ($#k5_group_1 :::"|^"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k5_group_1 :::"|^"::: ) (Set (Var "n"))))))))) ; theorem :: GROUP_4:2 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "H")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "h")))) "holds" (Bool (Set (Set (Var "a")) ($#k5_group_1 :::"|^"::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k5_group_1 :::"|^"::: ) (Set (Var "i"))))))))) ; theorem :: GROUP_4:3 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "a")) ($#r1_struct_0 :::"in"::: ) (Set (Var "H")))) "holds" (Bool (Set (Set (Var "a")) ($#k5_group_1 :::"|^"::: ) (Set (Var "n"))) ($#r1_struct_0 :::"in"::: ) (Set (Var "H"))))))) ; theorem :: GROUP_4:4 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "a")) ($#r1_struct_0 :::"in"::: ) (Set (Var "H")))) "holds" (Bool (Set (Set (Var "a")) ($#k5_group_1 :::"|^"::: ) (Set (Var "i"))) ($#r1_struct_0 :::"in"::: ) (Set (Var "H"))))))) ; definitionlet "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) ; let "F" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "G"))); func :::"Product"::: "F" -> ($#m1_subset_1 :::"Element":::) "of" "G" equals :: GROUP_4:def 2 (Set (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" "G") ($#k1_finsop_1 :::""**""::: ) "F"); end; :: deftheorem defines :::"Product"::: GROUP_4:def 2 : (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "holds" (Bool (Set ($#k3_group_4 :::"Product"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "G"))) ($#k1_finsop_1 :::""**""::: ) (Set (Var "F")))))); theorem :: GROUP_4:5 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#v3_group_1 :::"associative"::: ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "holds" (Bool (Set ($#k3_group_4 :::"Product"::: ) (Set "(" (Set (Var "F1")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "F2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_group_4 :::"Product"::: ) (Set (Var "F1")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" ($#k3_group_4 :::"Product"::: ) (Set (Var "F2")) ")" ))))) ; theorem :: GROUP_4:6 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k3_group_4 :::"Product"::: ) (Set "(" (Set (Var "F")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "a")) ($#k12_finseq_1 :::"*>"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_group_4 :::"Product"::: ) (Set (Var "F")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a"))))))) ; theorem :: GROUP_4:7 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#v3_group_1 :::"associative"::: ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k3_group_4 :::"Product"::: ) (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "a")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set "(" ($#k3_group_4 :::"Product"::: ) (Set (Var "F")) ")" )))))) ; theorem :: GROUP_4:8 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#l3_algstr_0 :::"multMagma"::: ) "holds" (Bool (Set ($#k3_group_4 :::"Product"::: ) (Set "(" ($#k6_finseq_1 :::"<*>"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "G"))))) ; theorem :: GROUP_4:9 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k3_group_4 :::"Product"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "a")) ($#k12_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "a"))))) ; theorem :: GROUP_4:10 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k3_group_4 :::"Product"::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b")))))) ; theorem :: GROUP_4:11 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set ($#k3_group_4 :::"Product"::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#k3_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "c")))) & (Bool (Set ($#k3_group_4 :::"Product"::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#k3_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "c")) ")" ))) ")" ))) ; theorem :: GROUP_4:12 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k3_group_4 :::"Product"::: ) (Set "(" (Set (Var "n")) ($#k5_finseq_2 :::"|->"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k5_group_1 :::"|^"::: ) (Set (Var "n"))))))) ; theorem :: GROUP_4:13 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "holds" (Bool (Set ($#k3_group_4 :::"Product"::: ) (Set "(" (Set (Var "F")) ($#k1_group_4 :::"-"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "G")) ")" ) ($#k6_domain_1 :::"}"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_group_4 :::"Product"::: ) (Set (Var "F")))))) ; theorem :: GROUP_4:14 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F2")))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F1"))))) "holds" (Bool (Set (Set (Var "F2")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "F1")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "k")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F1")) ($#k7_partfun1 :::"/."::: ) (Set (Var "k")) ")" ) ($#k2_group_1 :::"""::: ) )) ")" )) "holds" (Bool (Set ($#k3_group_4 :::"Product"::: ) (Set (Var "F1"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_group_4 :::"Product"::: ) (Set (Var "F2")) ")" ) ($#k2_group_1 :::"""::: ) )))) ; theorem :: GROUP_4:15 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "st" (Bool (Bool (Set (Var "G")) "is" ($#v5_group_1 :::"commutative"::: ) ($#l3_algstr_0 :::"Group":::))) "holds" (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "(" ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F1")) ")" ) "st" (Bool (Bool (Set (Var "F2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F1")) ($#k1_partfun1 :::"*"::: ) (Set (Var "P"))))) "holds" (Bool (Set ($#k3_group_4 :::"Product"::: ) (Set (Var "F1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_group_4 :::"Product"::: ) (Set (Var "F2"))))))) ; theorem :: GROUP_4:16 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "st" (Bool (Bool (Set (Var "G")) "is" ($#v5_group_1 :::"commutative"::: ) ($#l3_algstr_0 :::"Group":::)) & (Bool (Set (Var "F1")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set (Var "F2")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "F1"))) ($#r1_hidden :::"="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "F2"))))) "holds" (Bool (Set ($#k3_group_4 :::"Product"::: ) (Set (Var "F1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_group_4 :::"Product"::: ) (Set (Var "F2")))))) ; theorem :: GROUP_4:17 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "F")) "," (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "st" (Bool (Bool (Set (Var "G")) "is" ($#v5_group_1 :::"commutative"::: ) ($#l3_algstr_0 :::"Group":::)) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F1")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F2")))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F1")) ($#k7_partfun1 :::"/."::: ) (Set (Var "k")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "F2")) ($#k7_partfun1 :::"/."::: ) (Set (Var "k")) ")" ))) ")" )) "holds" (Bool (Set ($#k3_group_4 :::"Product"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_group_4 :::"Product"::: ) (Set (Var "F1")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" ($#k3_group_4 :::"Product"::: ) (Set (Var "F2")) ")" ))))) ; theorem :: GROUP_4:18 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "st" (Bool (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "F"))) ($#r1_tarski :::"c="::: ) (Set ($#k8_group_2 :::"carr"::: ) (Set (Var "H"))))) "holds" (Bool (Set ($#k3_group_4 :::"Product"::: ) (Set (Var "F"))) ($#r1_struct_0 :::"in"::: ) (Set (Var "H")))))) ; definitionlet "G" be ($#l3_algstr_0 :::"Group":::); let "I" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ); let "F" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "G"))); func "F" :::"|^"::: "I" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "G") means :: GROUP_4:def 3 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "F")) & (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "F"))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "F" ($#k7_partfun1 :::"/."::: ) (Set (Var "k")) ")" ) ($#k5_group_1 :::"|^"::: ) (Set "(" ($#k2_group_4 :::"@"::: ) (Set "(" "I" ($#k7_partfun1 :::"/."::: ) (Set (Var "k")) ")" ) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"|^"::: GROUP_4:def 3 : (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "I")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) (Bool "for" (Set (Var "F")) "," (Set (Var "b4")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k4_group_4 :::"|^"::: ) (Set (Var "I")))) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F")))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k7_partfun1 :::"/."::: ) (Set (Var "k")) ")" ) ($#k5_group_1 :::"|^"::: ) (Set "(" ($#k2_group_4 :::"@"::: ) (Set "(" (Set (Var "I")) ($#k7_partfun1 :::"/."::: ) (Set (Var "k")) ")" ) ")" ))) ")" ) ")" ) ")" )))); theorem :: GROUP_4:19 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) (Bool "for" (Set (Var "I1")) "," (Set (Var "I2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "I1")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F2"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "I2"))))) "holds" (Bool (Set (Set "(" (Set (Var "F1")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "F2")) ")" ) ($#k4_group_4 :::"|^"::: ) (Set "(" (Set (Var "I1")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "I2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F1")) ($#k4_group_4 :::"|^"::: ) (Set (Var "I1")) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" (Set (Var "F2")) ($#k4_group_4 :::"|^"::: ) (Set (Var "I2")) ")" )))))) ; theorem :: GROUP_4:20 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) (Bool "for" (Set (Var "I")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) "st" (Bool (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "F"))) ($#r1_tarski :::"c="::: ) (Set ($#k8_group_2 :::"carr"::: ) (Set (Var "H"))))) "holds" (Bool (Set ($#k3_group_4 :::"Product"::: ) (Set "(" (Set (Var "F")) ($#k4_group_4 :::"|^"::: ) (Set (Var "I")) ")" )) ($#r1_struct_0 :::"in"::: ) (Set (Var "H"))))))) ; theorem :: GROUP_4:21 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) "holds" (Bool (Set (Set "(" ($#k6_finseq_1 :::"<*>"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) ")" ) ($#k4_group_4 :::"|^"::: ) (Set "(" ($#k6_finseq_1 :::"<*>"::: ) (Set ($#k4_numbers :::"INT"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: GROUP_4:22 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "a")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k4_group_4 :::"|^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" ($#k2_group_4 :::"@"::: ) (Set (Var "i")) ")" ) ($#k12_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "a")) ($#k5_group_1 :::"|^"::: ) (Set (Var "i")) ")" ) ($#k12_finseq_1 :::"*>"::: ) ))))) ; theorem :: GROUP_4:23 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_finseq_4 :::"*>"::: ) ) ($#k4_group_4 :::"|^"::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set "(" ($#k2_group_4 :::"@"::: ) (Set (Var "i")) ")" ) "," (Set "(" ($#k2_group_4 :::"@"::: ) (Set (Var "j")) ")" ) ($#k2_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set "(" (Set (Var "a")) ($#k5_group_1 :::"|^"::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "b")) ($#k5_group_1 :::"|^"::: ) (Set (Var "j")) ")" ) ($#k2_finseq_4 :::"*>"::: ) ))))) ; theorem :: GROUP_4:24 (Bool "for" (Set (Var "i1")) "," (Set (Var "i2")) "," (Set (Var "i3")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#k3_finseq_4 :::"*>"::: ) ) ($#k4_group_4 :::"|^"::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set "(" ($#k2_group_4 :::"@"::: ) (Set (Var "i1")) ")" ) "," (Set "(" ($#k2_group_4 :::"@"::: ) (Set (Var "i2")) ")" ) "," (Set "(" ($#k2_group_4 :::"@"::: ) (Set (Var "i3")) ")" ) ($#k3_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set "(" (Set (Var "a")) ($#k5_group_1 :::"|^"::: ) (Set (Var "i1")) ")" ) "," (Set "(" (Set (Var "b")) ($#k5_group_1 :::"|^"::: ) (Set (Var "i2")) ")" ) "," (Set "(" (Set (Var "c")) ($#k5_group_1 :::"|^"::: ) (Set (Var "i3")) ")" ) ($#k3_finseq_4 :::"*>"::: ) ))))) ; theorem :: GROUP_4:25 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "holds" (Bool (Set (Set (Var "F")) ($#k4_group_4 :::"|^"::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "F")) ")" ) ($#k5_finseq_2 :::"|->"::: ) (Set "(" ($#k2_group_4 :::"@"::: ) (Num 1) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "F"))))) ; theorem :: GROUP_4:26 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "holds" (Bool (Set (Set (Var "F")) ($#k4_group_4 :::"|^"::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "F")) ")" ) ($#k5_finseq_2 :::"|->"::: ) (Set "(" ($#k2_group_4 :::"@"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "F")) ")" ) ($#k5_finseq_2 :::"|->"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "G")) ")" ))))) ; theorem :: GROUP_4:27 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "I")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "I"))) ($#r1_hidden :::"="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set "(" (Set (Var "n")) ($#k5_finseq_2 :::"|->"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "G")) ")" ) ")" ) ($#k4_group_4 :::"|^"::: ) (Set (Var "I"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k5_finseq_2 :::"|->"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "G")) ")" )))))) ; definitionlet "G" be ($#l3_algstr_0 :::"Group":::); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "G")); func :::"gr"::: "A" -> ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" "G" means :: GROUP_4:def 4 (Bool "(" (Bool "A" ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it)) & (Bool "(" "for" (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" "G" "st" (Bool (Bool "A" ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H"))))) "holds" (Bool it "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "H"))) ")" ) ")" ); end; :: deftheorem defines :::"gr"::: GROUP_4:def 4 : (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "b3")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k5_group_4 :::"gr"::: ) (Set (Var "A")))) "iff" (Bool "(" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b3")))) & (Bool "(" "for" (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H"))))) "holds" (Bool (Set (Var "b3")) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "H"))) ")" ) ")" ) ")" )))); theorem :: GROUP_4:28 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_struct_0 :::"in"::: ) (Set ($#k5_group_4 :::"gr"::: ) (Set (Var "A")))) "iff" (Bool "ex" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G")))(Bool "ex" (Set (Var "I")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "I")))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "F"))) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) & (Bool (Set ($#k3_group_4 :::"Product"::: ) (Set "(" (Set (Var "F")) ($#k4_group_4 :::"|^"::: ) (Set (Var "I")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" ))) ")" )))) ; theorem :: GROUP_4:29 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "a")) ($#r1_struct_0 :::"in"::: ) (Set ($#k5_group_4 :::"gr"::: ) (Set (Var "A"))))))) ; theorem :: GROUP_4:30 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) "holds" (Bool (Set ($#k5_group_4 :::"gr"::: ) (Set "(" ($#k1_subset_1 :::"{}"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) ")" )) ($#r1_group_2 :::"="::: ) (Set ($#k6_group_2 :::"(1)."::: ) (Set (Var "G"))))) ; theorem :: GROUP_4:31 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set ($#k5_group_4 :::"gr"::: ) (Set "(" ($#k8_group_2 :::"carr"::: ) (Set (Var "H")) ")" )) ($#r1_group_2 :::"="::: ) (Set (Var "H"))))) ; theorem :: GROUP_4:32 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set ($#k5_group_4 :::"gr"::: ) (Set (Var "A"))) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set ($#k5_group_4 :::"gr"::: ) (Set (Var "B")))))) ; theorem :: GROUP_4:33 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k5_group_4 :::"gr"::: ) (Set "(" (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B")) ")" )) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Set "(" ($#k5_group_4 :::"gr"::: ) (Set (Var "A")) ")" ) ($#k10_group_2 :::"/\"::: ) (Set "(" ($#k5_group_4 :::"gr"::: ) (Set (Var "B")) ")" ))))) ; theorem :: GROUP_4:34 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k5_group_4 :::"gr"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set (Var "B")) where B "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) : (Bool "ex" (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H")))) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k8_group_2 :::"carr"::: ) (Set (Var "H")))) ")" )) "}" )))) ; theorem :: GROUP_4:35 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k5_group_4 :::"gr"::: ) (Set (Var "A"))) ($#r1_group_2 :::"="::: ) (Set ($#k5_group_4 :::"gr"::: ) (Set "(" (Set (Var "A")) ($#k7_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "G")) ")" ) ($#k6_domain_1 :::"}"::: ) ) ")" ))))) ; definitionlet "G" be ($#l3_algstr_0 :::"Group":::); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G")); attr "a" is :::"generating"::: means :: GROUP_4:def 5 (Bool "ex" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" "G" "st" (Bool "(" (Bool (Set ($#k5_group_4 :::"gr"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "G") "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" "G") "#)" )) & (Bool (Bool "not" (Set ($#k5_group_4 :::"gr"::: ) (Set "(" (Set (Var "A")) ($#k7_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) "a" ($#k6_domain_1 :::"}"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "G") "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" "G") "#)" ))) ")" )); end; :: deftheorem defines :::"generating"::: GROUP_4:def 5 : (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "a")) "is" ($#v1_group_4 :::"generating"::: ) ) "iff" (Bool "ex" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set ($#k5_group_4 :::"gr"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "G"))) "#)" )) & (Bool (Bool "not" (Set ($#k5_group_4 :::"gr"::: ) (Set "(" (Set (Var "A")) ($#k7_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "a")) ($#k6_domain_1 :::"}"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "G"))) "#)" ))) ")" )) ")" ))); theorem :: GROUP_4:36 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) "holds" (Bool (Bool "not" (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "G"))) "is" ($#v1_group_4 :::"generating"::: ) ))) ; definitionlet "G" be ($#l3_algstr_0 :::"Group":::); let "H" be ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Const "G")); attr "H" is :::"maximal"::: means :: GROUP_4:def 6 (Bool "(" (Bool (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "H") "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" "H") "#)" ) ($#r1_hidden :::"<>"::: ) (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "G") "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" "G") "#)" )) & (Bool "(" "for" (Set (Var "K")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" "G" "st" (Bool (Bool (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "H") "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" "H") "#)" ) ($#r1_hidden :::"<>"::: ) (Set (Var "K"))) & (Bool "H" "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "K")))) "holds" (Bool (Set (Var "K")) ($#r1_hidden :::"="::: ) (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "G") "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" "G") "#)" )) ")" ) ")" ); end; :: deftheorem defines :::"maximal"::: GROUP_4:def 6 : (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "H")) "is" ($#v2_group_4 :::"maximal"::: ) ) "iff" (Bool "(" (Bool (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H"))) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "H"))) "#)" ) ($#r1_hidden :::"<>"::: ) (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "G"))) "#)" )) & (Bool "(" "for" (Set (Var "K")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H"))) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "H"))) "#)" ) ($#r1_hidden :::"<>"::: ) (Set (Var "K"))) & (Bool (Set (Var "H")) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "K")))) "holds" (Bool (Set (Var "K")) ($#r1_hidden :::"="::: ) (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "G"))) "#)" )) ")" ) ")" ) ")" ))); theorem :: GROUP_4:37 (Bool "for" (Set (Var "G")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "H")) "is" ($#v2_group_4 :::"maximal"::: ) ) & (Bool (Bool "not" (Set (Var "a")) ($#r1_struct_0 :::"in"::: ) (Set (Var "H"))))) "holds" (Bool (Set ($#k5_group_4 :::"gr"::: ) (Set "(" (Set "(" ($#k8_group_2 :::"carr"::: ) (Set (Var "H")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "a")) ($#k6_domain_1 :::"}"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "G")))))) ; definitionlet "G" be ($#l3_algstr_0 :::"Group":::); func :::"Phi"::: "G" -> ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" "G" means :: GROUP_4:def 7 (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set (Var "A")) where A "is" ($#m1_subset_1 :::"Subset":::) "of" "G" : (Bool "ex" (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" "G" "st" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H")))) & (Bool (Set (Var "H")) "is" ($#v2_group_4 :::"maximal"::: ) ) ")" )) "}" )) if (Bool "ex" (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" "G" "st" (Bool (Set (Var "H")) "is" ($#v2_group_4 :::"maximal"::: ) )) otherwise (Bool it ($#r1_hidden :::"="::: ) (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "G") "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" "G") "#)" )); end; :: deftheorem defines :::"Phi"::: GROUP_4:def 7 : (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "b2")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool "(" "(" (Bool (Bool "ex" (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Set (Var "H")) "is" ($#v2_group_4 :::"maximal"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k6_group_4 :::"Phi"::: ) (Set (Var "G")))) "iff" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set (Var "A")) where A "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) : (Bool "ex" (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H")))) & (Bool (Set (Var "H")) "is" ($#v2_group_4 :::"maximal"::: ) ) ")" )) "}" )) ")" ) ")" & "(" (Bool (Bool "(" "for" (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Bool "not" (Set (Var "H")) "is" ($#v2_group_4 :::"maximal"::: ) )) ")" )) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k6_group_4 :::"Phi"::: ) (Set (Var "G")))) "iff" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "G"))) "#)" )) ")" ) ")" ")" ))); theorem :: GROUP_4:38 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) "st" (Bool (Bool "ex" (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Set (Var "H")) "is" ($#v2_group_4 :::"maximal"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_struct_0 :::"in"::: ) (Set ($#k6_group_4 :::"Phi"::: ) (Set (Var "G")))) "iff" (Bool "for" (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "H")) "is" ($#v2_group_4 :::"maximal"::: ) )) "holds" (Bool (Set (Var "a")) ($#r1_struct_0 :::"in"::: ) (Set (Var "H")))) ")" )))) ; theorem :: GROUP_4:39 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool "(" "for" (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Bool "not" (Set (Var "H")) "is" ($#v2_group_4 :::"maximal"::: ) )) ")" )) "holds" (Bool (Set (Var "a")) ($#r1_struct_0 :::"in"::: ) (Set ($#k6_group_4 :::"Phi"::: ) (Set (Var "G")))))) ; theorem :: GROUP_4:40 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "H")) "is" ($#v2_group_4 :::"maximal"::: ) )) "holds" (Bool (Set ($#k6_group_4 :::"Phi"::: ) (Set (Var "G"))) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "H"))))) ; theorem :: GROUP_4:41 (Bool "for" (Set (Var "G")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#l3_algstr_0 :::"Group":::) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k6_group_4 :::"Phi"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) "{" (Set (Var "a")) where a "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) : (Bool (Bool "not" (Set (Var "a")) "is" ($#v1_group_4 :::"generating"::: ) )) "}" )) ; theorem :: GROUP_4:42 (Bool "for" (Set (Var "G")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_struct_0 :::"in"::: ) (Set ($#k6_group_4 :::"Phi"::: ) (Set (Var "G")))) "iff" (Bool (Bool "not" (Set (Var "a")) "is" ($#v1_group_4 :::"generating"::: ) )) ")" ))) ; definitionlet "G" be ($#l3_algstr_0 :::"Group":::); let "H1", "H2" be ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Const "G")); func "H1" :::"*"::: "H2" -> ($#m1_subset_1 :::"Subset":::) "of" "G" equals :: GROUP_4:def 8 (Set (Set "(" ($#k8_group_2 :::"carr"::: ) "H1" ")" ) ($#k2_group_2 :::"*"::: ) (Set "(" ($#k8_group_2 :::"carr"::: ) "H2" ")" )); end; :: deftheorem defines :::"*"::: GROUP_4:def 8 : (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "H1")) ($#k7_group_4 :::"*"::: ) (Set (Var "H2"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_group_2 :::"carr"::: ) (Set (Var "H1")) ")" ) ($#k2_group_2 :::"*"::: ) (Set "(" ($#k8_group_2 :::"carr"::: ) (Set (Var "H2")) ")" ))))); theorem :: GROUP_4:43 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Set (Var "H1")) ($#k7_group_4 :::"*"::: ) (Set (Var "H2"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_group_2 :::"carr"::: ) (Set (Var "H1")) ")" ) ($#k2_group_2 :::"*"::: ) (Set "(" ($#k8_group_2 :::"carr"::: ) (Set (Var "H2")) ")" ))) & (Bool (Set (Set (Var "H1")) ($#k7_group_4 :::"*"::: ) (Set (Var "H2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "H1")) ($#k12_group_2 :::"*"::: ) (Set "(" ($#k8_group_2 :::"carr"::: ) (Set (Var "H2")) ")" ))) & (Bool (Set (Set (Var "H1")) ($#k7_group_4 :::"*"::: ) (Set (Var "H2"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_group_2 :::"carr"::: ) (Set (Var "H1")) ")" ) ($#k11_group_2 :::"*"::: ) (Set (Var "H2")))) ")" ))) ; theorem :: GROUP_4:44 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "," (Set (Var "H3")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" (Set (Var "H1")) ($#k7_group_4 :::"*"::: ) (Set (Var "H2")) ")" ) ($#k11_group_2 :::"*"::: ) (Set (Var "H3"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "H1")) ($#k12_group_2 :::"*"::: ) (Set "(" (Set (Var "H2")) ($#k7_group_4 :::"*"::: ) (Set (Var "H3")) ")" ))))) ; theorem :: GROUP_4:45 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k13_group_2 :::"*"::: ) (Set (Var "H1")) ")" ) ($#k11_group_2 :::"*"::: ) (Set (Var "H2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k4_group_2 :::"*"::: ) (Set "(" (Set (Var "H1")) ($#k7_group_4 :::"*"::: ) (Set (Var "H2")) ")" )))))) ; theorem :: GROUP_4:46 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" (Set (Var "H1")) ($#k7_group_4 :::"*"::: ) (Set (Var "H2")) ")" ) ($#k5_group_2 :::"*"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "H1")) ($#k12_group_2 :::"*"::: ) (Set "(" (Set (Var "H2")) ($#k14_group_2 :::"*"::: ) (Set (Var "a")) ")" )))))) ; theorem :: GROUP_4:47 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k11_group_2 :::"*"::: ) (Set (Var "H1")) ")" ) ($#k11_group_2 :::"*"::: ) (Set (Var "H2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k2_group_2 :::"*"::: ) (Set "(" (Set (Var "H1")) ($#k7_group_4 :::"*"::: ) (Set (Var "H2")) ")" )))))) ; theorem :: GROUP_4:48 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" (Set (Var "H1")) ($#k7_group_4 :::"*"::: ) (Set (Var "H2")) ")" ) ($#k2_group_2 :::"*"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "H1")) ($#k12_group_2 :::"*"::: ) (Set "(" (Set (Var "H2")) ($#k12_group_2 :::"*"::: ) (Set (Var "A")) ")" )))))) ; definitionlet "G" be ($#l3_algstr_0 :::"Group":::); let "H1", "H2" be ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Const "G")); func "H1" :::""\/""::: "H2" -> ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" "G" equals :: GROUP_4:def 9 (Set ($#k5_group_4 :::"gr"::: ) (Set "(" (Set "(" ($#k8_group_2 :::"carr"::: ) "H1" ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k8_group_2 :::"carr"::: ) "H2" ")" ) ")" )); end; :: deftheorem defines :::""\/""::: GROUP_4:def 9 : (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "H1")) ($#k8_group_4 :::""\/""::: ) (Set (Var "H2"))) ($#r1_hidden :::"="::: ) (Set ($#k5_group_4 :::"gr"::: ) (Set "(" (Set "(" ($#k8_group_2 :::"carr"::: ) (Set (Var "H1")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k8_group_2 :::"carr"::: ) (Set (Var "H2")) ")" ) ")" ))))); theorem :: GROUP_4:49 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_struct_0 :::"in"::: ) (Set (Set (Var "H1")) ($#k8_group_4 :::""\/""::: ) (Set (Var "H2")))) "iff" (Bool "ex" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G")))(Bool "ex" (Set (Var "I")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "I")))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "F"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k8_group_2 :::"carr"::: ) (Set (Var "H1")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k8_group_2 :::"carr"::: ) (Set (Var "H2")) ")" ))) & (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k3_group_4 :::"Product"::: ) (Set "(" (Set (Var "F")) ($#k4_group_4 :::"|^"::: ) (Set (Var "I")) ")" ))) ")" ))) ")" )))) ; theorem :: GROUP_4:50 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "H1")) ($#k8_group_4 :::""\/""::: ) (Set (Var "H2"))) ($#r1_group_2 :::"="::: ) (Set ($#k5_group_4 :::"gr"::: ) (Set "(" (Set (Var "H1")) ($#k7_group_4 :::"*"::: ) (Set (Var "H2")) ")" ))))) ; theorem :: GROUP_4:51 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Set (Var "H1")) ($#k7_group_4 :::"*"::: ) (Set (Var "H2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "H2")) ($#k7_group_4 :::"*"::: ) (Set (Var "H1"))))) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" (Set (Var "H1")) ($#k8_group_4 :::""\/""::: ) (Set (Var "H2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "H1")) ($#k7_group_4 :::"*"::: ) (Set (Var "H2")))))) ; theorem :: GROUP_4:52 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v5_group_1 :::"commutative"::: ) ($#l3_algstr_0 :::"Group":::))) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" (Set (Var "H1")) ($#k8_group_4 :::""\/""::: ) (Set (Var "H2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "H1")) ($#k7_group_4 :::"*"::: ) (Set (Var "H2")))))) ; theorem :: GROUP_4:53 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "N1")) "," (Set (Var "N2")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" (Set (Var "N1")) ($#k8_group_4 :::""\/""::: ) (Set (Var "N2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "N1")) ($#k7_group_4 :::"*"::: ) (Set (Var "N2")))))) ; theorem :: GROUP_4:54 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "N1")) "," (Set (Var "N2")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "N1")) ($#k8_group_4 :::""\/""::: ) (Set (Var "N2"))) "is" ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G"))))) ; theorem :: GROUP_4:55 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "H")) ($#k8_group_4 :::""\/""::: ) (Set (Var "H"))) ($#r1_group_2 :::"="::: ) (Set (Var "H"))))) ; theorem :: GROUP_4:56 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "H1")) ($#k8_group_4 :::""\/""::: ) (Set (Var "H2"))) ($#r1_group_2 :::"="::: ) (Set (Set (Var "H2")) ($#k8_group_4 :::""\/""::: ) (Set (Var "H1")))))) ; theorem :: GROUP_4:57 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "," (Set (Var "H3")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" (Set (Var "H1")) ($#k8_group_4 :::""\/""::: ) (Set (Var "H2")) ")" ) ($#k8_group_4 :::""\/""::: ) (Set (Var "H3"))) ($#r1_group_2 :::"="::: ) (Set (Set (Var "H1")) ($#k8_group_4 :::""\/""::: ) (Set "(" (Set (Var "H2")) ($#k8_group_4 :::""\/""::: ) (Set (Var "H3")) ")" ))))) ; theorem :: GROUP_4:58 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k6_group_2 :::"(1)."::: ) (Set (Var "G")) ")" ) ($#k8_group_4 :::""\/""::: ) (Set (Var "H"))) ($#r1_group_2 :::"="::: ) (Set (Var "H"))) & (Bool (Set (Set (Var "H")) ($#k8_group_4 :::""\/""::: ) (Set "(" ($#k6_group_2 :::"(1)."::: ) (Set (Var "G")) ")" )) ($#r1_group_2 :::"="::: ) (Set (Var "H"))) ")" ))) ; theorem :: GROUP_4:59 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k7_group_2 :::"(Omega)."::: ) (Set (Var "G")) ")" ) ($#k8_group_4 :::""\/""::: ) (Set (Var "H"))) ($#r1_group_2 :::"="::: ) (Set ($#k7_group_2 :::"(Omega)."::: ) (Set (Var "G")))) & (Bool (Set (Set (Var "H")) ($#k8_group_4 :::""\/""::: ) (Set "(" ($#k7_group_2 :::"(Omega)."::: ) (Set (Var "G")) ")" )) ($#r1_group_2 :::"="::: ) (Set ($#k7_group_2 :::"(Omega)."::: ) (Set (Var "G")))) ")" ))) ; theorem :: GROUP_4:60 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "H1")) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Set (Var "H1")) ($#k8_group_4 :::""\/""::: ) (Set (Var "H2")))) & (Bool (Set (Var "H2")) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Set (Var "H1")) ($#k8_group_4 :::""\/""::: ) (Set (Var "H2")))) ")" ))) ; theorem :: GROUP_4:61 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H1")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "H2")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "H1")) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "H2"))) "iff" (Bool (Set (Set (Var "H1")) ($#k8_group_4 :::""\/""::: ) (Set (Var "H2"))) ($#r1_group_2 :::"="::: ) (Set (Var "H2"))) ")" )))) ; theorem :: GROUP_4:62 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "," (Set (Var "H3")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "H1")) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "H2")))) "holds" (Bool (Set (Var "H1")) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Set (Var "H2")) ($#k8_group_4 :::""\/""::: ) (Set (Var "H3")))))) ; theorem :: GROUP_4:63 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "H3")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "H1")) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "H3"))) & (Bool (Set (Var "H2")) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "H3")))) "holds" (Bool (Set (Set (Var "H1")) ($#k8_group_4 :::""\/""::: ) (Set (Var "H2"))) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "H3")))))) ; theorem :: GROUP_4:64 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H1")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "H3")) "," (Set (Var "H2")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "H1")) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "H2")))) "holds" (Bool (Set (Set (Var "H1")) ($#k8_group_4 :::""\/""::: ) (Set (Var "H3"))) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Set (Var "H2")) ($#k8_group_4 :::""\/""::: ) (Set (Var "H3"))))))) ; theorem :: GROUP_4:65 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "H1")) ($#k10_group_2 :::"/\"::: ) (Set (Var "H2"))) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Set (Var "H1")) ($#k8_group_4 :::""\/""::: ) (Set (Var "H2")))))) ; theorem :: GROUP_4:66 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H1")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "H2")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" (Set (Var "H1")) ($#k10_group_2 :::"/\"::: ) (Set (Var "H2")) ")" ) ($#k8_group_4 :::""\/""::: ) (Set (Var "H2"))) ($#r1_group_2 :::"="::: ) (Set (Var "H2")))))) ; theorem :: GROUP_4:67 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H2")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "H1")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "H1")) ($#k10_group_2 :::"/\"::: ) (Set "(" (Set (Var "H1")) ($#k8_group_4 :::""\/""::: ) (Set (Var "H2")) ")" )) ($#r1_group_2 :::"="::: ) (Set (Var "H1")))))) ; theorem :: GROUP_4:68 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Set (Var "H1")) ($#k8_group_4 :::""\/""::: ) (Set (Var "H2"))) ($#r1_group_2 :::"="::: ) (Set (Var "H2"))) "iff" (Bool (Set (Set (Var "H1")) ($#k10_group_2 :::"/\"::: ) (Set (Var "H2"))) ($#r1_group_2 :::"="::: ) (Set (Var "H1"))) ")" ))) ; definitionlet "G" be ($#l3_algstr_0 :::"Group":::); func :::"SubJoin"::: "G" -> ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k1_group_3 :::"Subgroups"::: ) "G" ")" ) means :: GROUP_4:def 10 (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" "G" "holds" (Bool (Set it ($#k1_binop_1 :::"."::: ) "(" (Set (Var "H1")) "," (Set (Var "H2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "H1")) ($#k8_group_4 :::""\/""::: ) (Set (Var "H2"))))); end; :: deftheorem defines :::"SubJoin"::: GROUP_4:def 10 : (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k1_group_3 :::"Subgroups"::: ) (Set (Var "G")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k9_group_4 :::"SubJoin"::: ) (Set (Var "G")))) "iff" (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "b2")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "H1")) "," (Set (Var "H2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "H1")) ($#k8_group_4 :::""\/""::: ) (Set (Var "H2"))))) ")" ))); definitionlet "G" be ($#l3_algstr_0 :::"Group":::); func :::"SubMeet"::: "G" -> ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k1_group_3 :::"Subgroups"::: ) "G" ")" ) means :: GROUP_4:def 11 (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" "G" "holds" (Bool (Set it ($#k1_binop_1 :::"."::: ) "(" (Set (Var "H1")) "," (Set (Var "H2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "H1")) ($#k10_group_2 :::"/\"::: ) (Set (Var "H2"))))); end; :: deftheorem defines :::"SubMeet"::: GROUP_4:def 11 : (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k1_group_3 :::"Subgroups"::: ) (Set (Var "G")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k10_group_4 :::"SubMeet"::: ) (Set (Var "G")))) "iff" (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "b2")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "H1")) "," (Set (Var "H2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "H1")) ($#k10_group_2 :::"/\"::: ) (Set (Var "H2"))))) ")" ))); definitionlet "G" be ($#l3_algstr_0 :::"Group":::); func :::"lattice"::: "G" -> ($#v3_lattices :::"strict"::: ) ($#l3_lattices :::"Lattice":::) equals :: GROUP_4:def 12 (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "(" ($#k1_group_3 :::"Subgroups"::: ) "G" ")" ) "," (Set "(" ($#k9_group_4 :::"SubJoin"::: ) "G" ")" ) "," (Set "(" ($#k10_group_4 :::"SubMeet"::: ) "G" ")" ) "#)" ); end; :: deftheorem defines :::"lattice"::: GROUP_4:def 12 : (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) "holds" (Bool (Set ($#k11_group_4 :::"lattice"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "(" ($#k1_group_3 :::"Subgroups"::: ) (Set (Var "G")) ")" ) "," (Set "(" ($#k9_group_4 :::"SubJoin"::: ) (Set (Var "G")) ")" ) "," (Set "(" ($#k10_group_4 :::"SubMeet"::: ) (Set (Var "G")) ")" ) "#)" ))); theorem :: GROUP_4:69 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k11_group_4 :::"lattice"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_group_3 :::"Subgroups"::: ) (Set (Var "G"))))) ; theorem :: GROUP_4:70 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) "holds" (Bool (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set "(" ($#k11_group_4 :::"lattice"::: ) (Set (Var "G")) ")" )) ($#r1_funct_2 :::"="::: ) (Set ($#k9_group_4 :::"SubJoin"::: ) (Set (Var "G"))))) ; theorem :: GROUP_4:71 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) "holds" (Bool (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set "(" ($#k11_group_4 :::"lattice"::: ) (Set (Var "G")) ")" )) ($#r1_funct_2 :::"="::: ) (Set ($#k10_group_4 :::"SubMeet"::: ) (Set (Var "G"))))) ; registrationlet "G" be ($#l3_algstr_0 :::"Group":::); cluster (Set ($#k11_group_4 :::"lattice"::: ) "G") -> ($#v3_lattices :::"strict"::: ) ($#v13_lattices :::"lower-bounded"::: ) ($#v14_lattices :::"upper-bounded"::: ) ; end; theorem :: GROUP_4:72 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) "holds" (Bool (Set ($#k5_lattices :::"Bottom"::: ) (Set "(" ($#k11_group_4 :::"lattice"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_group_2 :::"(1)."::: ) (Set (Var "G"))))) ; theorem :: GROUP_4:73 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) "holds" (Bool (Set ($#k6_lattices :::"Top"::: ) (Set "(" ($#k11_group_4 :::"lattice"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_group_2 :::"(Omega)."::: ) (Set (Var "G"))))) ;