Proofgold Proposition

∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 . Group (pack_b x0 x1) ⟶ x2 ⊆ x0 ⟶ explicit_Group_identity x0 x1 ∈ x2 ⟶ (∀ x3 . x3 ∈ x2 ⟶ explicit_Group_inverse x0 x1 x3 ∈ x2) ⟶ (∀ x3 . x3 ∈ x2 ⟶ ∀ x4 . x4 ∈ x2 ⟶ x1 x3 x4 ∈ x2) ⟶ explicit_subgroup x0 x1 x2

type
prop

theory
HotG

name
explicit_subgroup_test

proof
PUMaE..

Megalodon
explicit_subgroup_test

proofgold address
TMSe5..^{explicit_subgroup_test}

creator
4924 Pr6Pc../82509..

owner
4924 Pr6Pc../82509..

term root
a0764..