Proofgold Proposition

∀ x0 x1 x2 . Field_extension_by_1 x0 x1 x2 ⟶ ∀ x3 : ο . (subfield x0 x1 ⟶ x2 ∈ setminus (field0 x1) (field0 x0) ⟶ (∀ x4 . subfield x0 x4 ⟶ x2 ∈ field0 x4 ⟶ subfield x1 x4) ⟶ x3) ⟶ x3

type
prop

theory
HotG

name
Field_extension_by_1_E

proof
PUXQg..

Megalodon
Field_extension_by_1_E

proofgold address
TMFdx..^{Field_extension_by_1_E}

creator
5919 Pr6Pc../19f99..

owner
5919 Pr6Pc../19f99..

term root
338a5..