### Nuprl Lemma : r2-eu_wf

`EuclideanPlane(ℝ^2) ∈ EuclideanPlane`

Proof

Definitions occuring in Statement :  r2-eu: `EuclideanPlane(ℝ^2)` euclidean-plane: `EuclideanPlane` member: `t ∈ T`
Definitions unfolded in proof :  r2-eu: `EuclideanPlane(ℝ^2)` uall: `∀[x:A]. B[x]` member: `t ∈ T` geo-gt-prim: `ab>cd` geo-point: `Point` r2-eu-prim: `r2-eu-prim()` mk-eu-prim: mk-eu-prim all: `∀x:A. B[x]` eq_atom: `x =a y` ifthenelse: `if b then t else f fi ` bfalse: `ff` btrue: `tt` subtype_rel: `A ⊆r B` prop: `ℙ` nat: `ℕ` le: `A ≤ B` and: `P ∧ Q` less_than': `less_than'(a;b)` not: `¬A` implies: `P `` Q` false: `False` geo-lsep: `a # bc` geo-left: `a leftof bc` geo-sep: `a # b` geo-between: `B(abc)` geo-colinear: `Colinear(a;b;c)` geo-congruent: `ab ≅ cd` geo-length-sep: `ab # cd)` circle-strict-overlap: `StrictOverlap(a;b;c;d)` uimplies: `b supposing a`

Latex:
EuclideanPlane(\mBbbR{}\^{}2)  \mmember{}  EuclideanPlane

Date html generated: 2020_05_20-PM-01_10_33
Last ObjectModification: 2020_02_07-PM-04_26_35

Theory : reals!model!euclidean!geometry

Home Index