:: LATSUBGR semantic presentation begin theorem :: LATSUBGR:1 (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 "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" (Set (Var "H1")) ($#k10_group_2 :::"/\"::: ) (Set (Var "H2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H1"))) ($#k3_xboole_0 :::"/\"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H2"))))))) ; theorem :: LATSUBGR:2 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "h")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "h")) ($#r2_hidden :::"in"::: ) (Set ($#k1_group_3 :::"Subgroups"::: ) (Set (Var "G")))) "iff" (Bool "ex" (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set (Var "H")))) ")" ))) ; theorem :: LATSUBGR:3 (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 "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"))))) "holds" (Bool (Set ($#k5_group_4 :::"gr"::: ) (Set (Var "A"))) ($#r1_group_2 :::"="::: ) (Set (Var "H")))))) ; theorem :: LATSUBGR:4 (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 "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H1"))) ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H2")))))) "holds" (Bool (Set (Set (Var "H1")) ($#k8_group_4 :::""\/""::: ) (Set (Var "H2"))) ($#r1_group_2 :::"="::: ) (Set ($#k5_group_4 :::"gr"::: ) (Set (Var "A"))))))) ; theorem :: LATSUBGR:5 (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 "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool "(" (Bool (Set (Var "g")) ($#r1_struct_0 :::"in"::: ) (Set (Var "H1"))) "or" (Bool (Set (Var "g")) ($#r1_struct_0 :::"in"::: ) (Set (Var "H2"))) ")" )) "holds" (Bool (Set (Var "g")) ($#r1_struct_0 :::"in"::: ) (Set (Set (Var "H1")) ($#k8_group_4 :::""\/""::: ) (Set (Var "H2"))))))) ; theorem :: LATSUBGR:6 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G1")) "," (Set (Var "G2")) (Bool "for" (Set (Var "H1")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G1")) (Bool "ex" (Set (Var "H2")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G2")) "st" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H1"))))))))) ; theorem :: LATSUBGR:7 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G1")) "," (Set (Var "G2")) (Bool "for" (Set (Var "H2")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G2")) (Bool "ex" (Set (Var "H1")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G1")) "st" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H2"))))))))) ; theorem :: LATSUBGR:8 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G1")) "," (Set (Var "G2")) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G1")) (Bool "for" (Set (Var "H3")) "," (Set (Var "H4")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G2")) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H3"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H1"))))) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H4"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H2"))))) & (Bool (Set (Var "H1")) "is" ($#m1_group_6 :::"Subgroup"::: ) "of" (Set (Var "H2")))) "holds" (Bool (Set (Var "H3")) "is" ($#m1_group_6 :::"Subgroup"::: ) "of" (Set (Var "H4"))))))) ; theorem :: LATSUBGR:9 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G1")) "," (Set (Var "G2")) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G2")) (Bool "for" (Set (Var "H3")) "," (Set (Var "H4")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G1")) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H3"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H1"))))) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H4"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H2"))))) & (Bool (Set (Var "H1")) "is" ($#m1_group_6 :::"Subgroup"::: ) "of" (Set (Var "H2")))) "holds" (Bool (Set (Var "H3")) "is" ($#m1_group_6 :::"Subgroup"::: ) "of" (Set (Var "H4"))))))) ; theorem :: LATSUBGR:10 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G1"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G2"))) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G1")) "holds" (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k5_group_4 :::"gr"::: ) (Set (Var "A")) ")" ))))))) ; theorem :: LATSUBGR:11 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G1")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G1"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G2"))) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G1")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H1"))) ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H2")))))) "holds" (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" (Set (Var "H1")) ($#k8_group_4 :::""\/""::: ) (Set (Var "H2")) ")" ))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k5_group_4 :::"gr"::: ) (Set (Var "A")) ")" )))))))) ; theorem :: LATSUBGR:12 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "G")) ")" ) ($#k1_tarski :::"}"::: ) ))) "holds" (Bool (Set ($#k5_group_4 :::"gr"::: ) (Set (Var "A"))) ($#r1_group_2 :::"="::: ) (Set ($#k6_group_2 :::"(1)."::: ) (Set (Var "G")))))) ; definitionlet "G" be ($#l3_algstr_0 :::"Group":::); func :::"carr"::: "G" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k1_group_3 :::"Subgroups"::: ) "G" ")" ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "G") ")" ) means :: LATSUBGR:def 1 (Bool "for" (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" "G" "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H"))))); end; :: deftheorem defines :::"carr"::: LATSUBGR:def 1 : (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k1_group_3 :::"Subgroups"::: ) (Set (Var "G")) ")" ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_latsubgr :::"carr"::: ) (Set (Var "G")))) "iff" (Bool "for" (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H"))))) ")" ))); theorem :: LATSUBGR:13 (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")) (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 "(" ($#k1_latsubgr :::"carr"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "H")))) "iff" (Bool (Set (Var "x")) ($#r1_struct_0 :::"in"::: ) (Set (Var "H"))) ")" )))) ; theorem :: LATSUBGR:14 (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 ($#k1_group_1 :::"1_"::: ) (Set (Var "G"))) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k1_latsubgr :::"carr"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "H")))))) ; theorem :: LATSUBGR:15 (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 "(" ($#k1_latsubgr :::"carr"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "H"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: LATSUBGR:16 (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")) (Bool "for" (Set (Var "g1")) "," (Set (Var "g2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "g1")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k1_latsubgr :::"carr"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "H")))) & (Bool (Set (Var "g2")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k1_latsubgr :::"carr"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "H"))))) "holds" (Bool (Set (Set (Var "g1")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "g2"))) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k1_latsubgr :::"carr"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "H"))))))) ; theorem :: LATSUBGR:17 (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")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k1_latsubgr :::"carr"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "H"))))) "holds" (Bool (Set (Set (Var "g")) ($#k2_group_1 :::"""::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k1_latsubgr :::"carr"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "H"))))))) ; theorem :: LATSUBGR:18 (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 (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" (Set (Var "H1")) ($#k10_group_2 :::"/\"::: ) (Set (Var "H2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_latsubgr :::"carr"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "H1")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" (Set "(" ($#k1_latsubgr :::"carr"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "H2")) ")" ))))) ; theorem :: LATSUBGR:19 (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 (Set (Set "(" ($#k1_latsubgr :::"carr"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "H1")) ($#k10_group_2 :::"/\"::: ) (Set (Var "H2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_latsubgr :::"carr"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "H1")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" (Set "(" ($#k1_latsubgr :::"carr"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "H2")) ")" ))))) ; definitionlet "G" be ($#l3_algstr_0 :::"Group":::); let "F" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_group_3 :::"Subgroups"::: ) (Set (Const "G")) ")" ); func :::"meet"::: "F" -> ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" "G" means :: LATSUBGR:def 2 (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k6_setfam_1 :::"meet"::: ) (Set "(" (Set "(" ($#k1_latsubgr :::"carr"::: ) "G" ")" ) ($#k7_relset_1 :::".:"::: ) "F" ")" ))); end; :: deftheorem defines :::"meet"::: LATSUBGR:def 2 : (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "F")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_group_3 :::"Subgroups"::: ) (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 ($#k2_latsubgr :::"meet"::: ) (Set (Var "F")))) "iff" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k6_setfam_1 :::"meet"::: ) (Set "(" (Set "(" ($#k1_latsubgr :::"carr"::: ) (Set (Var "G")) ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "F")) ")" ))) ")" )))); theorem :: LATSUBGR:20 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "F")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_group_3 :::"Subgroups"::: ) (Set (Var "G")) ")" ) "st" (Bool (Bool (Set ($#k6_group_2 :::"(1)."::: ) (Set (Var "G"))) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool (Set ($#k2_latsubgr :::"meet"::: ) (Set (Var "F"))) ($#r1_group_2 :::"="::: ) (Set ($#k6_group_2 :::"(1)."::: ) (Set (Var "G")))))) ; theorem :: LATSUBGR:21 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_group_3 :::"Subgroups"::: ) (Set (Var "G"))) (Bool "for" (Set (Var "F")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_group_3 :::"Subgroups"::: ) (Set (Var "G")) ")" ) "st" (Bool (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "h")) ($#k1_tarski :::"}"::: ) ))) "holds" (Bool (Set ($#k2_latsubgr :::"meet"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Var "h")))))) ; theorem :: LATSUBGR:22 (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 "h1")) "," (Set (Var "h2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k11_group_4 :::"lattice"::: ) (Set (Var "G")) ")" ) "st" (Bool (Bool (Set (Var "h1")) ($#r1_hidden :::"="::: ) (Set (Var "H1"))) & (Bool (Set (Var "h2")) ($#r1_hidden :::"="::: ) (Set (Var "H2")))) "holds" (Bool (Set (Set (Var "h1")) ($#k3_lattices :::""\/""::: ) (Set (Var "h2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "H1")) ($#k8_group_4 :::""\/""::: ) (Set (Var "H2"))))))) ; theorem :: LATSUBGR:23 (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 "h1")) "," (Set (Var "h2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k11_group_4 :::"lattice"::: ) (Set (Var "G")) ")" ) "st" (Bool (Bool (Set (Var "h1")) ($#r1_hidden :::"="::: ) (Set (Var "H1"))) & (Bool (Set (Var "h2")) ($#r1_hidden :::"="::: ) (Set (Var "H2")))) "holds" (Bool (Set (Set (Var "h1")) ($#k4_lattices :::""/\""::: ) (Set (Var "h2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "H1")) ($#k10_group_2 :::"/\"::: ) (Set (Var "H2"))))))) ; theorem :: LATSUBGR:24 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k11_group_4 :::"lattice"::: ) (Set (Var "G")) ")" ) (Bool "for" (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "H")))) "holds" (Bool (Set (Var "H")) "is" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")))))) ; theorem :: LATSUBGR:25 (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 "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k11_group_4 :::"lattice"::: ) (Set (Var "G")) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "H1"))) & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Var "H2")))) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r3_lattices :::"[="::: ) (Set (Var "q"))) "iff" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H1"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H2")))) ")" )))) ; theorem :: LATSUBGR:26 (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 "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k11_group_4 :::"lattice"::: ) (Set (Var "G")) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "H1"))) & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Var "H2")))) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r3_lattices :::"[="::: ) (Set (Var "q"))) "iff" (Bool (Set (Var "H1")) "is" ($#m1_group_6 :::"Subgroup"::: ) "of" (Set (Var "H2"))) ")" )))) ; theorem :: LATSUBGR:27 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) "holds" (Bool (Set ($#k11_group_4 :::"lattice"::: ) (Set (Var "G"))) "is" ($#v4_lattice3 :::"complete"::: ) )) ; definitionlet "G1", "G2" be ($#l3_algstr_0 :::"Group":::); let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "G1"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "G2"))); func :::"FuncLatt"::: "f" -> ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k11_group_4 :::"lattice"::: ) "G1" ")" )) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k11_group_4 :::"lattice"::: ) "G2" ")" )) means :: LATSUBGR:def 3 (Bool "for" (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" "G1" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" "G2" "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set "f" ($#k7_relset_1 :::".:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H")))))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set ($#k5_group_4 :::"gr"::: ) (Set (Var "A")))))); end; :: deftheorem defines :::"FuncLatt"::: LATSUBGR:def 3 : (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G1"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G2"))) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k11_group_4 :::"lattice"::: ) (Set (Var "G1")) ")" )) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k11_group_4 :::"lattice"::: ) (Set (Var "G2")) ")" )) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k3_latsubgr :::"FuncLatt"::: ) (Set (Var "f")))) "iff" (Bool "for" (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G1")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G2")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H")))))) "holds" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set ($#k5_group_4 :::"gr"::: ) (Set (Var "A")))))) ")" )))); theorem :: LATSUBGR:28 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) "holds" (Bool (Set ($#k3_latsubgr :::"FuncLatt"::: ) (Set "(" ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k11_group_4 :::"lattice"::: ) (Set (Var "G")) ")" ))))) ; theorem :: LATSUBGR:29 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G1")) "," (Set (Var "G2")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) "holds" (Bool (Set ($#k3_latsubgr :::"FuncLatt"::: ) (Set (Var "f"))) "is" ($#v2_funct_1 :::"one-to-one"::: ) ))) ; theorem :: LATSUBGR:30 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G1")) "," (Set (Var "G2")) "holds" (Bool (Set (Set "(" ($#k3_latsubgr :::"FuncLatt"::: ) (Set (Var "f")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k6_group_2 :::"(1)."::: ) (Set (Var "G1")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_group_2 :::"(1)."::: ) (Set (Var "G2")))))) ; theorem :: LATSUBGR:31 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G1")) "," (Set (Var "G2")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) "holds" (Bool (Set ($#k3_latsubgr :::"FuncLatt"::: ) (Set (Var "f"))) "is" ($#m3_vectsp_8 :::"Semilattice-Homomorphism"::: ) "of" (Set ($#k11_group_4 :::"lattice"::: ) (Set (Var "G1"))) "," (Set ($#k11_group_4 :::"lattice"::: ) (Set (Var "G2")))))) ; theorem :: LATSUBGR:32 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G1")) "," (Set (Var "G2")) "holds" (Bool (Set ($#k3_latsubgr :::"FuncLatt"::: ) (Set (Var "f"))) "is" ($#m4_vectsp_8 :::"sup-Semilattice-Homomorphism"::: ) "of" (Set ($#k11_group_4 :::"lattice"::: ) (Set (Var "G1"))) "," (Set ($#k11_group_4 :::"lattice"::: ) (Set (Var "G2")))))) ; theorem :: LATSUBGR:33 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G1")) "," (Set (Var "G2")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) "holds" (Bool (Set ($#k3_latsubgr :::"FuncLatt"::: ) (Set (Var "f"))) "is" ($#m1_lattice4 :::"Homomorphism"::: ) "of" (Set ($#k11_group_4 :::"lattice"::: ) (Set (Var "G1"))) "," (Set ($#k11_group_4 :::"lattice"::: ) (Set (Var "G2")))))) ;