:: GROUP_11 semantic presentation begin theorem :: GROUP_11:1 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "N")) "being" ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" (Set (Var "x1")) ($#k13_group_2 :::"*"::: ) (Set (Var "N")) ")" ) ($#k2_group_2 :::"*"::: ) (Set "(" (Set (Var "x2")) ($#k13_group_2 :::"*"::: ) (Set (Var "N")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x1")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x2")) ")" ) ($#k13_group_2 :::"*"::: ) (Set (Var "N"))))))) ; theorem :: GROUP_11:2 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "N")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "x")) ($#k13_group_2 :::"*"::: ) (Set (Var "N"))))) "holds" (Bool (Set (Set (Var "x")) ($#k13_group_2 :::"*"::: ) (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k13_group_2 :::"*"::: ) (Set (Var "N"))))))) ; theorem :: GROUP_11:3 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "N")) "," (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Set (Var "x")) ($#k13_group_2 :::"*"::: ) (Set (Var "N"))) ($#r1_xboole_0 :::"meets"::: ) (Set ($#k8_group_2 :::"carr"::: ) (Set (Var "H"))))) "holds" (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "x")) ($#k13_group_2 :::"*"::: ) (Set (Var "N")))) & (Bool (Set (Var "y")) ($#r1_struct_0 :::"in"::: ) (Set (Var "H"))) ")" ))))) ; theorem :: GROUP_11:4 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "N")) "being" ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "y")) ($#r1_struct_0 :::"in"::: ) (Set (Var "N")))) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k2_group_1 :::"""::: ) ")" )) ($#r1_struct_0 :::"in"::: ) (Set (Var "N")))))) ; theorem :: GROUP_11:5 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "N")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "y")) ($#r1_struct_0 :::"in"::: ) (Set (Var "N")))) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k2_group_1 :::"""::: ) ")" )) ($#r1_struct_0 :::"in"::: ) (Set (Var "N"))) ")" )) "holds" (Bool (Set (Var "N")) "is" ($#v1_group_3 :::"normal"::: ) ))) ; theorem :: GROUP_11:6 (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 "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "H1")) ($#k7_group_4 :::"*"::: ) (Set (Var "H2")))) "iff" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b")))) & (Bool (Set (Var "a")) ($#r1_struct_0 :::"in"::: ) (Set (Var "H1"))) & (Bool (Set (Var "b")) ($#r1_struct_0 :::"in"::: ) (Set (Var "H2"))) ")" )) ")" )))) ; theorem :: GROUP_11:7 (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")) (Bool "ex" (Set (Var "M")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "N1")) ($#k7_group_4 :::"*"::: ) (Set (Var "N2"))))))) ; theorem :: GROUP_11:8 (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")) (Bool "ex" (Set (Var "M")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "N1")) ($#k7_group_4 :::"*"::: ) (Set (Var "N2"))))))) ; theorem :: GROUP_11:9 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "N")) "," (Set (Var "N1")) "," (Set (Var "N2")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "N1")) ($#k7_group_4 :::"*"::: ) (Set (Var "N2"))))) "holds" (Bool "(" (Bool (Set (Var "N1")) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "N"))) & (Bool (Set (Var "N2")) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "N"))) ")" ))) ; theorem :: GROUP_11:10 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "N")) "," (Set (Var "N1")) "," (Set (Var "N2")) "being" ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "N1")) ($#k7_group_4 :::"*"::: ) (Set (Var "N2"))))) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k13_group_2 :::"*"::: ) (Set (Var "N1")) ")" ) ($#k2_group_2 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k13_group_2 :::"*"::: ) (Set (Var "N2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b")) ")" ) ($#k13_group_2 :::"*"::: ) (Set (Var "N"))))))) ; theorem :: GROUP_11:11 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "N")) "being" ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k13_group_2 :::"*"::: ) (Set (Var "N")) ")" ) ($#k5_group_2 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k2_group_1 :::"""::: ) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k8_group_2 :::"carr"::: ) (Set (Var "N"))))))) ; definitionlet "G" be ($#l3_algstr_0 :::"Group":::); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "G")); let "N" be ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Const "G")); func "N" :::"`"::: "A" -> ($#m1_subset_1 :::"Subset":::) "of" "G" equals :: GROUP_11:def 1 "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element":::) "of" "G" : (Bool (Set (Set (Var "x")) ($#k13_group_2 :::"*"::: ) "N") ($#r1_tarski :::"c="::: ) "A") "}" ; func "N" :::"~"::: "A" -> ($#m1_subset_1 :::"Subset":::) "of" "G" equals :: GROUP_11:def 2 "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element":::) "of" "G" : (Bool (Set (Set (Var "x")) ($#k13_group_2 :::"*"::: ) "N") ($#r1_xboole_0 :::"meets"::: ) "A") "}" ; end; :: deftheorem defines :::"`"::: GROUP_11:def 1 : (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 "N")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "N")) ($#k1_group_11 :::"`"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) : (Bool (Set (Set (Var "x")) ($#k13_group_2 :::"*"::: ) (Set (Var "N"))) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) "}" )))); :: deftheorem defines :::"~"::: GROUP_11:def 2 : (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 "N")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "N")) ($#k2_group_11 :::"~"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) : (Bool (Set (Set (Var "x")) ($#k13_group_2 :::"*"::: ) (Set (Var "N"))) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "A"))) "}" )))); theorem :: GROUP_11:12 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "N")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "N")) ($#k1_group_11 :::"`"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Set (Var "x")) ($#k13_group_2 :::"*"::: ) (Set (Var "N"))) ($#r1_tarski :::"c="::: ) (Set (Var "A"))))))) ; theorem :: GROUP_11:13 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "N")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Set (Var "x")) ($#k13_group_2 :::"*"::: ) (Set (Var "N"))) ($#r1_tarski :::"c="::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "N")) ($#k1_group_11 :::"`"::: ) (Set (Var "A")))))))) ; theorem :: GROUP_11:14 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "N")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "N")) ($#k2_group_11 :::"~"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Set (Var "x")) ($#k13_group_2 :::"*"::: ) (Set (Var "N"))) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "A"))))))) ; theorem :: GROUP_11:15 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "N")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Set (Var "x")) ($#k13_group_2 :::"*"::: ) (Set (Var "N"))) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "N")) ($#k2_group_11 :::"~"::: ) (Set (Var "A")))))))) ; theorem :: GROUP_11:16 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "N")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "N")) ($#k1_group_11 :::"`"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set (Var "A")))))) ; theorem :: GROUP_11:17 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "N")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "N")) ($#k2_group_11 :::"~"::: ) (Set (Var "A"))))))) ; theorem :: GROUP_11:18 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "N")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "N")) ($#k1_group_11 :::"`"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "N")) ($#k2_group_11 :::"~"::: ) (Set (Var "A"))))))) ; theorem :: GROUP_11:19 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "N")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "N")) ($#k2_group_11 :::"~"::: ) (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "N")) ($#k2_group_11 :::"~"::: ) (Set (Var "A")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set (Var "N")) ($#k2_group_11 :::"~"::: ) (Set (Var "B")) ")" )))))) ; theorem :: GROUP_11:20 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "N")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "N")) ($#k1_group_11 :::"`"::: ) (Set "(" (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "N")) ($#k1_group_11 :::"`"::: ) (Set (Var "A")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set (Var "N")) ($#k1_group_11 :::"`"::: ) (Set (Var "B")) ")" )))))) ; theorem :: GROUP_11:21 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "N")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set (Set (Var "N")) ($#k1_group_11 :::"`"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "N")) ($#k1_group_11 :::"`"::: ) (Set (Var "B"))))))) ; theorem :: GROUP_11:22 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "N")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set (Set (Var "N")) ($#k2_group_11 :::"~"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "N")) ($#k2_group_11 :::"~"::: ) (Set (Var "B"))))))) ; theorem :: GROUP_11:23 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "N")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" (Set (Var "N")) ($#k1_group_11 :::"`"::: ) (Set (Var "A")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set (Var "N")) ($#k1_group_11 :::"`"::: ) (Set (Var "B")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set (Var "N")) ($#k1_group_11 :::"`"::: ) (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B")) ")" )))))) ; theorem :: GROUP_11:24 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "N")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "N")) ($#k2_group_11 :::"~"::: ) (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "N")) ($#k2_group_11 :::"~"::: ) (Set (Var "A")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set (Var "N")) ($#k2_group_11 :::"~"::: ) (Set (Var "B")) ")" )))))) ; theorem :: GROUP_11:25 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "N")) "," (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "N")) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "H")))) "holds" (Bool (Set (Set (Var "H")) ($#k1_group_11 :::"`"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "N")) ($#k1_group_11 :::"`"::: ) (Set (Var "A"))))))) ; theorem :: GROUP_11:26 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "N")) "," (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "N")) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "H")))) "holds" (Bool (Set (Set (Var "N")) ($#k2_group_11 :::"~"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "H")) ($#k2_group_11 :::"~"::: ) (Set (Var "A"))))))) ; theorem :: GROUP_11:27 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "N")) "being" ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" (Set (Var "N")) ($#k1_group_11 :::"`"::: ) (Set (Var "A")) ")" ) ($#k2_group_2 :::"*"::: ) (Set "(" (Set (Var "N")) ($#k1_group_11 :::"`"::: ) (Set (Var "B")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set (Var "N")) ($#k1_group_11 :::"`"::: ) (Set "(" (Set (Var "A")) ($#k2_group_2 :::"*"::: ) (Set (Var "B")) ")" )))))) ; theorem :: GROUP_11:28 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "N")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "N")) ($#k2_group_11 :::"~"::: ) (Set "(" (Set (Var "A")) ($#k2_group_2 :::"*"::: ) (Set (Var "B")) ")" )))) "holds" (Bool (Set (Set (Var "x")) ($#k13_group_2 :::"*"::: ) (Set (Var "N"))) ($#r1_xboole_0 :::"meets"::: ) (Set (Set (Var "A")) ($#k2_group_2 :::"*"::: ) (Set (Var "B")))))))) ; theorem :: GROUP_11:29 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "N")) "being" ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" (Set (Var "N")) ($#k2_group_11 :::"~"::: ) (Set (Var "A")) ")" ) ($#k2_group_2 :::"*"::: ) (Set "(" (Set (Var "N")) ($#k2_group_11 :::"~"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "N")) ($#k2_group_11 :::"~"::: ) (Set "(" (Set (Var "A")) ($#k2_group_2 :::"*"::: ) (Set (Var "B")) ")" )))))) ; theorem :: GROUP_11:30 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "N")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "N")) ($#k2_group_11 :::"~"::: ) (Set "(" (Set (Var "N")) ($#k1_group_11 :::"`"::: ) (Set "(" (Set (Var "N")) ($#k2_group_11 :::"~"::: ) (Set (Var "A")) ")" ) ")" )))) "holds" (Bool (Set (Set (Var "x")) ($#k13_group_2 :::"*"::: ) (Set (Var "N"))) ($#r1_xboole_0 :::"meets"::: ) (Set (Set (Var "N")) ($#k1_group_11 :::"`"::: ) (Set "(" (Set (Var "N")) ($#k2_group_11 :::"~"::: ) (Set (Var "A")) ")" ))))))) ; theorem :: GROUP_11:31 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "N")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "N")) ($#k1_group_11 :::"`"::: ) (Set "(" (Set (Var "N")) ($#k2_group_11 :::"~"::: ) (Set (Var "A")) ")" )))) "holds" (Bool (Set (Set (Var "x")) ($#k13_group_2 :::"*"::: ) (Set (Var "N"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "N")) ($#k2_group_11 :::"~"::: ) (Set (Var "A")))))))) ; theorem :: GROUP_11:32 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "N")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "N")) ($#k2_group_11 :::"~"::: ) (Set "(" (Set (Var "N")) ($#k2_group_11 :::"~"::: ) (Set (Var "A")) ")" )))) "holds" (Bool (Set (Set (Var "x")) ($#k13_group_2 :::"*"::: ) (Set (Var "N"))) ($#r1_xboole_0 :::"meets"::: ) (Set (Set (Var "N")) ($#k2_group_11 :::"~"::: ) (Set (Var "A")))))))) ; theorem :: GROUP_11:33 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "N")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "N")) ($#k2_group_11 :::"~"::: ) (Set "(" (Set (Var "N")) ($#k1_group_11 :::"`"::: ) (Set (Var "A")) ")" )))) "holds" (Bool (Set (Set (Var "x")) ($#k13_group_2 :::"*"::: ) (Set (Var "N"))) ($#r1_xboole_0 :::"meets"::: ) (Set (Set (Var "N")) ($#k1_group_11 :::"`"::: ) (Set (Var "A")))))))) ; theorem :: GROUP_11:34 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "N")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "N")) ($#k1_group_11 :::"`"::: ) (Set "(" (Set (Var "N")) ($#k1_group_11 :::"`"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "N")) ($#k1_group_11 :::"`"::: ) (Set (Var "A"))))))) ; theorem :: GROUP_11:35 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "N")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "N")) ($#k2_group_11 :::"~"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "N")) ($#k2_group_11 :::"~"::: ) (Set "(" (Set (Var "N")) ($#k2_group_11 :::"~"::: ) (Set (Var "A")) ")" )))))) ; theorem :: GROUP_11:36 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "N")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "N")) ($#k1_group_11 :::"`"::: ) (Set "(" (Set (Var "N")) ($#k1_group_11 :::"`"::: ) (Set (Var "A")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set (Var "N")) ($#k2_group_11 :::"~"::: ) (Set "(" (Set (Var "N")) ($#k2_group_11 :::"~"::: ) (Set (Var "A")) ")" )))))) ; theorem :: GROUP_11:37 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "N")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "N")) ($#k2_group_11 :::"~"::: ) (Set "(" (Set (Var "N")) ($#k1_group_11 :::"`"::: ) (Set (Var "A")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "A")))))) ; theorem :: GROUP_11:38 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "N")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "N")) ($#k1_group_11 :::"`"::: ) (Set "(" (Set (Var "N")) ($#k2_group_11 :::"~"::: ) (Set "(" (Set (Var "N")) ($#k1_group_11 :::"`"::: ) (Set (Var "A")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "N")) ($#k1_group_11 :::"`"::: ) (Set (Var "A"))))))) ; theorem :: GROUP_11:39 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "N")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "N")) ($#k1_group_11 :::"`"::: ) (Set "(" (Set (Var "N")) ($#k2_group_11 :::"~"::: ) (Set (Var "A")) ")" )))) "holds" (Bool (Set (Set (Var "N")) ($#k2_group_11 :::"~"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "N")) ($#k2_group_11 :::"~"::: ) (Set "(" (Set (Var "N")) ($#k1_group_11 :::"`"::: ) (Set "(" (Set (Var "N")) ($#k2_group_11 :::"~"::: ) (Set (Var "A")) ")" ) ")" )))))) ; theorem :: GROUP_11:40 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "N")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "N")) ($#k2_group_11 :::"~"::: ) (Set "(" (Set (Var "N")) ($#k1_group_11 :::"`"::: ) (Set "(" (Set (Var "N")) ($#k2_group_11 :::"~"::: ) (Set (Var "A")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "N")) ($#k2_group_11 :::"~"::: ) (Set (Var "A"))))))) ; theorem :: GROUP_11:41 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "N")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "N")) ($#k1_group_11 :::"`"::: ) (Set "(" (Set (Var "N")) ($#k1_group_11 :::"`"::: ) (Set (Var "A")) ")" )))) "holds" (Bool (Set (Set (Var "x")) ($#k13_group_2 :::"*"::: ) (Set (Var "N"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "N")) ($#k1_group_11 :::"`"::: ) (Set (Var "A")))))))) ; theorem :: GROUP_11:42 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "N")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "N")) ($#k1_group_11 :::"`"::: ) (Set "(" (Set (Var "N")) ($#k1_group_11 :::"`"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "N")) ($#k2_group_11 :::"~"::: ) (Set "(" (Set (Var "N")) ($#k1_group_11 :::"`"::: ) (Set (Var "A")) ")" )))))) ; theorem :: GROUP_11:43 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "N")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "N")) ($#k2_group_11 :::"~"::: ) (Set "(" (Set (Var "N")) ($#k2_group_11 :::"~"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "N")) ($#k1_group_11 :::"`"::: ) (Set "(" (Set (Var "N")) ($#k2_group_11 :::"~"::: ) (Set (Var "A")) ")" )))))) ; theorem :: GROUP_11:44 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "N")) "," (Set (Var "N1")) "," (Set (Var "N2")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "N")) ($#r1_hidden :::"="::: ) (Set (Set (Var "N1")) ($#k10_group_2 :::"/\"::: ) (Set (Var "N2"))))) "holds" (Bool (Set (Set (Var "N")) ($#k2_group_11 :::"~"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "N1")) ($#k2_group_11 :::"~"::: ) (Set (Var "A")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set (Var "N2")) ($#k2_group_11 :::"~"::: ) (Set (Var "A")) ")" )))))) ; theorem :: GROUP_11:45 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "N")) "," (Set (Var "N1")) "," (Set (Var "N2")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "N")) ($#r1_hidden :::"="::: ) (Set (Set (Var "N1")) ($#k10_group_2 :::"/\"::: ) (Set (Var "N2"))))) "holds" (Bool (Set (Set "(" (Set (Var "N1")) ($#k1_group_11 :::"`"::: ) (Set (Var "A")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set (Var "N2")) ($#k1_group_11 :::"`"::: ) (Set (Var "A")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set (Var "N")) ($#k1_group_11 :::"`"::: ) (Set (Var "A"))))))) ; theorem :: GROUP_11:46 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (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")) (Bool "ex" (Set (Var "N")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "N1")) ($#k7_group_4 :::"*"::: ) (Set (Var "N2")))) & (Bool (Set (Set (Var "N")) ($#k1_group_11 :::"`"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "N1")) ($#k1_group_11 :::"`"::: ) (Set (Var "A")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set (Var "N2")) ($#k1_group_11 :::"`"::: ) (Set (Var "A")) ")" ))) ")" ))))) ; theorem :: GROUP_11:47 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (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")) (Bool "ex" (Set (Var "N")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "N1")) ($#k7_group_4 :::"*"::: ) (Set (Var "N2")))) & (Bool (Set (Set "(" (Set (Var "N1")) ($#k2_group_11 :::"~"::: ) (Set (Var "A")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set (Var "N2")) ($#k2_group_11 :::"~"::: ) (Set (Var "A")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set (Var "N")) ($#k2_group_11 :::"~"::: ) (Set (Var "A")))) ")" ))))) ; theorem :: GROUP_11:48 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (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")) (Bool "ex" (Set (Var "N")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "N1")) ($#k7_group_4 :::"*"::: ) (Set (Var "N2")))) & (Bool (Set (Set (Var "N")) ($#k2_group_11 :::"~"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set "(" (Set (Var "N1")) ($#k2_group_11 :::"~"::: ) (Set (Var "A")) ")" ) ($#k11_group_2 :::"*"::: ) (Set (Var "N2")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set "(" (Set (Var "N2")) ($#k2_group_11 :::"~"::: ) (Set (Var "A")) ")" ) ($#k11_group_2 :::"*"::: ) (Set (Var "N1")) ")" ))) ")" ))))) ; definitionlet "G" be ($#l3_algstr_0 :::"Group":::); let "H", "N" be ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Const "G")); func "N" :::"`"::: "H" -> ($#m1_subset_1 :::"Subset":::) "of" "G" equals :: GROUP_11:def 3 "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element":::) "of" "G" : (Bool (Set (Set (Var "x")) ($#k13_group_2 :::"*"::: ) "N") ($#r1_tarski :::"c="::: ) (Set ($#k8_group_2 :::"carr"::: ) "H")) "}" ; func "N" :::"~"::: "H" -> ($#m1_subset_1 :::"Subset":::) "of" "G" equals :: GROUP_11:def 4 "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element":::) "of" "G" : (Bool (Set (Set (Var "x")) ($#k13_group_2 :::"*"::: ) "N") ($#r1_xboole_0 :::"meets"::: ) (Set ($#k8_group_2 :::"carr"::: ) "H")) "}" ; end; :: deftheorem defines :::"`"::: GROUP_11:def 3 : (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H")) "," (Set (Var "N")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "N")) ($#k3_group_11 :::"`"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) : (Bool (Set (Set (Var "x")) ($#k13_group_2 :::"*"::: ) (Set (Var "N"))) ($#r1_tarski :::"c="::: ) (Set ($#k8_group_2 :::"carr"::: ) (Set (Var "H")))) "}" ))); :: deftheorem defines :::"~"::: GROUP_11:def 4 : (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H")) "," (Set (Var "N")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "N")) ($#k4_group_11 :::"~"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) : (Bool (Set (Set (Var "x")) ($#k13_group_2 :::"*"::: ) (Set (Var "N"))) ($#r1_xboole_0 :::"meets"::: ) (Set ($#k8_group_2 :::"carr"::: ) (Set (Var "H")))) "}" ))); theorem :: GROUP_11:49 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "N")) "," (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "N")) ($#k3_group_11 :::"`"::: ) (Set (Var "H"))))) "holds" (Bool (Set (Set (Var "x")) ($#k13_group_2 :::"*"::: ) (Set (Var "N"))) ($#r1_tarski :::"c="::: ) (Set ($#k8_group_2 :::"carr"::: ) (Set (Var "H"))))))) ; theorem :: GROUP_11:50 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "N")) "," (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Set (Var "x")) ($#k13_group_2 :::"*"::: ) (Set (Var "N"))) ($#r1_tarski :::"c="::: ) (Set ($#k8_group_2 :::"carr"::: ) (Set (Var "H"))))) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "N")) ($#k3_group_11 :::"`"::: ) (Set (Var "H"))))))) ; theorem :: GROUP_11:51 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "N")) "," (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "N")) ($#k4_group_11 :::"~"::: ) (Set (Var "H"))))) "holds" (Bool (Set (Set (Var "x")) ($#k13_group_2 :::"*"::: ) (Set (Var "N"))) ($#r1_xboole_0 :::"meets"::: ) (Set ($#k8_group_2 :::"carr"::: ) (Set (Var "H"))))))) ; theorem :: GROUP_11:52 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "N")) "," (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Set (Var "x")) ($#k13_group_2 :::"*"::: ) (Set (Var "N"))) ($#r1_xboole_0 :::"meets"::: ) (Set ($#k8_group_2 :::"carr"::: ) (Set (Var "H"))))) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "N")) ($#k4_group_11 :::"~"::: ) (Set (Var "H"))))))) ; theorem :: GROUP_11:53 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "N")) "," (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "N")) ($#k3_group_11 :::"`"::: ) (Set (Var "H"))) ($#r1_tarski :::"c="::: ) (Set ($#k8_group_2 :::"carr"::: ) (Set (Var "H")))))) ; theorem :: GROUP_11:54 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H")) "," (Set (Var "N")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set ($#k8_group_2 :::"carr"::: ) (Set (Var "H"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "N")) ($#k4_group_11 :::"~"::: ) (Set (Var "H")))))) ; theorem :: GROUP_11:55 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "N")) "," (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "N")) ($#k3_group_11 :::"`"::: ) (Set (Var "H"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "N")) ($#k4_group_11 :::"~"::: ) (Set (Var "H")))))) ; theorem :: GROUP_11:56 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "," (Set (Var "N")) "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 (Set (Var "N")) ($#k4_group_11 :::"~"::: ) (Set (Var "H1"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "N")) ($#k4_group_11 :::"~"::: ) (Set (Var "H2")))))) ; theorem :: GROUP_11:57 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H")) "," (Set (Var "N1")) "," (Set (Var "N2")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "N1")) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "N2")))) "holds" (Bool (Set (Set (Var "N1")) ($#k4_group_11 :::"~"::: ) (Set (Var "H"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "N2")) ($#k4_group_11 :::"~"::: ) (Set (Var "H")))))) ; theorem :: GROUP_11:58 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "N1")) "," (Set (Var "N2")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "N1")) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "N2")))) "holds" (Bool (Set (Set (Var "N1")) ($#k4_group_11 :::"~"::: ) (Set (Var "N1"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "N2")) ($#k4_group_11 :::"~"::: ) (Set (Var "N2")))))) ; theorem :: GROUP_11:59 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "," (Set (Var "N")) "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 (Set (Var "N")) ($#k3_group_11 :::"`"::: ) (Set (Var "H1"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "N")) ($#k3_group_11 :::"`"::: ) (Set (Var "H2")))))) ; theorem :: GROUP_11:60 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H")) "," (Set (Var "N1")) "," (Set (Var "N2")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "N1")) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "N2")))) "holds" (Bool (Set (Set (Var "N2")) ($#k3_group_11 :::"`"::: ) (Set (Var "H"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "N1")) ($#k3_group_11 :::"`"::: ) (Set (Var "H")))))) ; theorem :: GROUP_11:61 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "N1")) "," (Set (Var "N2")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "N1")) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "N2")))) "holds" (Bool (Set (Set (Var "N2")) ($#k3_group_11 :::"`"::: ) (Set (Var "N1"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "N1")) ($#k3_group_11 :::"`"::: ) (Set (Var "N2")))))) ; theorem :: GROUP_11:62 (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 "N")) "being" ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" (Set (Var "N")) ($#k3_group_11 :::"`"::: ) (Set (Var "H1")) ")" ) ($#k2_group_2 :::"*"::: ) (Set "(" (Set (Var "N")) ($#k3_group_11 :::"`"::: ) (Set (Var "H2")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set (Var "N")) ($#k1_group_11 :::"`"::: ) (Set "(" (Set (Var "H1")) ($#k7_group_4 :::"*"::: ) (Set (Var "H2")) ")" )))))) ; theorem :: GROUP_11: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 "N")) "being" ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" (Set (Var "N")) ($#k4_group_11 :::"~"::: ) (Set (Var "H1")) ")" ) ($#k2_group_2 :::"*"::: ) (Set "(" (Set (Var "N")) ($#k4_group_11 :::"~"::: ) (Set (Var "H2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "N")) ($#k2_group_11 :::"~"::: ) (Set "(" (Set (Var "H1")) ($#k7_group_4 :::"*"::: ) (Set (Var "H2")) ")" )))))) ; theorem :: GROUP_11:64 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H")) "," (Set (Var "N")) "," (Set (Var "N1")) "," (Set (Var "N2")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "N")) ($#r1_hidden :::"="::: ) (Set (Set (Var "N1")) ($#k10_group_2 :::"/\"::: ) (Set (Var "N2"))))) "holds" (Bool (Set (Set (Var "N")) ($#k4_group_11 :::"~"::: ) (Set (Var "H"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "N1")) ($#k4_group_11 :::"~"::: ) (Set (Var "H")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set (Var "N2")) ($#k4_group_11 :::"~"::: ) (Set (Var "H")) ")" ))))) ; theorem :: GROUP_11:65 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H")) "," (Set (Var "N")) "," (Set (Var "N1")) "," (Set (Var "N2")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "N")) ($#r1_hidden :::"="::: ) (Set (Set (Var "N1")) ($#k10_group_2 :::"/\"::: ) (Set (Var "N2"))))) "holds" (Bool (Set (Set "(" (Set (Var "N1")) ($#k3_group_11 :::"`"::: ) (Set (Var "H")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set (Var "N2")) ($#k3_group_11 :::"`"::: ) (Set (Var "H")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set (Var "N")) ($#k3_group_11 :::"`"::: ) (Set (Var "H")))))) ; theorem :: GROUP_11:66 (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 "N1")) "," (Set (Var "N2")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "ex" (Set (Var "N")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "N1")) ($#k7_group_4 :::"*"::: ) (Set (Var "N2")))) & (Bool (Set (Set (Var "N")) ($#k3_group_11 :::"`"::: ) (Set (Var "H"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "N1")) ($#k3_group_11 :::"`"::: ) (Set (Var "H")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set (Var "N2")) ($#k3_group_11 :::"`"::: ) (Set (Var "H")) ")" ))) ")" ))))) ; theorem :: GROUP_11:67 (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 "N1")) "," (Set (Var "N2")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "ex" (Set (Var "N")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "N1")) ($#k7_group_4 :::"*"::: ) (Set (Var "N2")))) & (Bool (Set (Set "(" (Set (Var "N1")) ($#k4_group_11 :::"~"::: ) (Set (Var "H")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set (Var "N2")) ($#k4_group_11 :::"~"::: ) (Set (Var "H")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set (Var "N")) ($#k4_group_11 :::"~"::: ) (Set (Var "H")))) ")" ))))) ; theorem :: GROUP_11:68 (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 "N1")) "," (Set (Var "N2")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "ex" (Set (Var "N")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "N1")) ($#k7_group_4 :::"*"::: ) (Set (Var "N2")))) & (Bool (Set (Set "(" (Set (Var "N1")) ($#k3_group_11 :::"`"::: ) (Set (Var "H")) ")" ) ($#k2_group_2 :::"*"::: ) (Set "(" (Set (Var "N2")) ($#k3_group_11 :::"`"::: ) (Set (Var "H")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set (Var "N")) ($#k3_group_11 :::"`"::: ) (Set (Var "H")))) ")" ))))) ; theorem :: GROUP_11:69 (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 "N1")) "," (Set (Var "N2")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "ex" (Set (Var "N")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "N1")) ($#k7_group_4 :::"*"::: ) (Set (Var "N2")))) & (Bool (Set (Set "(" (Set (Var "N1")) ($#k4_group_11 :::"~"::: ) (Set (Var "H")) ")" ) ($#k2_group_2 :::"*"::: ) (Set "(" (Set (Var "N2")) ($#k4_group_11 :::"~"::: ) (Set (Var "H")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set (Var "N")) ($#k4_group_11 :::"~"::: ) (Set (Var "H")))) ")" ))))) ; theorem :: GROUP_11:70 (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 "N1")) "," (Set (Var "N2")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "ex" (Set (Var "N")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "N1")) ($#k7_group_4 :::"*"::: ) (Set (Var "N2")))) & (Bool (Set (Set (Var "N")) ($#k4_group_11 :::"~"::: ) (Set (Var "H"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set "(" (Set (Var "N1")) ($#k4_group_11 :::"~"::: ) (Set (Var "H")) ")" ) ($#k11_group_2 :::"*"::: ) (Set (Var "N2")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set "(" (Set (Var "N2")) ($#k4_group_11 :::"~"::: ) (Set (Var "H")) ")" ) ($#k11_group_2 :::"*"::: ) (Set (Var "N1")) ")" ))) ")" ))))) ; theorem :: GROUP_11:71 (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 "N")) "being" ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "ex" (Set (Var "M")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "N")) ($#k4_group_11 :::"~"::: ) (Set (Var "H")))))))) ; theorem :: GROUP_11:72 (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 "N")) "being" ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "N")) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "H")))) "holds" (Bool "ex" (Set (Var "M")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "N")) ($#k3_group_11 :::"`"::: ) (Set (Var "H")))))))) ; theorem :: GROUP_11:73 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H")) "," (Set (Var "N")) "being" ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "ex" (Set (Var "M")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "N")) ($#k4_group_11 :::"~"::: ) (Set (Var "H"))))))) ; theorem :: GROUP_11:74 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H")) "," (Set (Var "N")) "being" ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "N")) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "H")))) "holds" (Bool "ex" (Set (Var "M")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "N")) ($#k3_group_11 :::"`"::: ) (Set (Var "H"))))))) ; theorem :: GROUP_11:75 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "N")) "," (Set (Var "N1")) "being" ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "N1")) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "N")))) "holds" (Bool "ex" (Set (Var "N2")) "," (Set (Var "N3")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "N1")) ($#k4_group_11 :::"~"::: ) (Set (Var "N")))) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N3"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "N1")) ($#k3_group_11 :::"`"::: ) (Set (Var "N")))) & (Bool (Set (Set (Var "N2")) ($#k3_group_11 :::"`"::: ) (Set (Var "N"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "N3")) ($#k3_group_11 :::"`"::: ) (Set (Var "N")))) ")" )))) ; theorem :: GROUP_11:76 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "N")) "," (Set (Var "N1")) "being" ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "N1")) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "N")))) "holds" (Bool "ex" (Set (Var "N2")) "," (Set (Var "N3")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "N1")) ($#k4_group_11 :::"~"::: ) (Set (Var "N")))) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N3"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "N1")) ($#k3_group_11 :::"`"::: ) (Set (Var "N")))) & (Bool (Set (Set (Var "N3")) ($#k4_group_11 :::"~"::: ) (Set (Var "N"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "N2")) ($#k4_group_11 :::"~"::: ) (Set (Var "N")))) ")" )))) ; theorem :: GROUP_11:77 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "N")) "," (Set (Var "N1")) "being" ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "N1")) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "N")))) "holds" (Bool "ex" (Set (Var "N2")) "," (Set (Var "N3")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "N1")) ($#k4_group_11 :::"~"::: ) (Set (Var "N")))) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N3"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "N1")) ($#k3_group_11 :::"`"::: ) (Set (Var "N")))) & (Bool (Set (Set (Var "N2")) ($#k3_group_11 :::"`"::: ) (Set (Var "N"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "N3")) ($#k4_group_11 :::"~"::: ) (Set (Var "N")))) ")" )))) ; theorem :: GROUP_11:78 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "N")) "," (Set (Var "N1")) "being" ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "N1")) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "N")))) "holds" (Bool "ex" (Set (Var "N2")) "," (Set (Var "N3")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "N1")) ($#k4_group_11 :::"~"::: ) (Set (Var "N")))) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N3"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "N1")) ($#k3_group_11 :::"`"::: ) (Set (Var "N")))) & (Bool (Set (Set (Var "N3")) ($#k3_group_11 :::"`"::: ) (Set (Var "N"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "N2")) ($#k4_group_11 :::"~"::: ) (Set (Var "N")))) ")" )))) ; theorem :: GROUP_11:79 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "N")) "," (Set (Var "N1")) "," (Set (Var "N2")) "being" ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "N1")) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "N2")))) "holds" (Bool "ex" (Set (Var "N3")) "," (Set (Var "N4")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N3"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "N")) ($#k4_group_11 :::"~"::: ) (Set (Var "N1")))) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N4"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "N")) ($#k4_group_11 :::"~"::: ) (Set (Var "N2")))) & (Bool (Set (Set (Var "N3")) ($#k4_group_11 :::"~"::: ) (Set (Var "N1"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "N4")) ($#k4_group_11 :::"~"::: ) (Set (Var "N1")))) ")" )))) ; theorem :: GROUP_11:80 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "N")) "," (Set (Var "N1")) "being" ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "ex" (Set (Var "N2")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "N")) ($#k3_group_11 :::"`"::: ) (Set (Var "N")))) & (Bool (Set (Set (Var "N")) ($#k3_group_11 :::"`"::: ) (Set (Var "N1"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "N2")) ($#k3_group_11 :::"`"::: ) (Set (Var "N1")))) ")" )))) ; theorem :: GROUP_11:81 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "N")) "," (Set (Var "N1")) "being" ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "ex" (Set (Var "N2")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "N")) ($#k4_group_11 :::"~"::: ) (Set (Var "N")))) & (Bool (Set (Set (Var "N")) ($#k4_group_11 :::"~"::: ) (Set (Var "N1"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "N2")) ($#k4_group_11 :::"~"::: ) (Set (Var "N1")))) ")" )))) ;