Proofgold Proposition

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

type
prop

theory
HotG

name
Field_extension_by_1_I

proof
PUXQg..

Megalodon
Field_extension_by_1_I

proofgold address
TMPm9..^{Field_extension_by_1_I}

creator
5919 Pr6Pc../7f347..

owner
5919 Pr6Pc../7f347..

term root
b32e9..