Nuprl Lemma : eu-bisect-angle_wf

`∀e:EuclideanPlane. ∀a,b,c:Point.  (eu-bisect-angle(e;a;b;c) ∈ ℙ)`

Proof

Definitions occuring in Statement :  eu-bisect-angle: `eu-bisect-angle(e;a;b;c)` euclidean-plane: `EuclideanPlane` eu-point: `Point` prop: `ℙ` all: `∀x:A. B[x]` member: `t ∈ T`
Definitions unfolded in proof :  all: `∀x:A. B[x]` member: `t ∈ T` eu-bisect-angle: `eu-bisect-angle(e;a;b;c)` prop: `ℙ` and: `P ∧ Q` uall: `∀[x:A]. B[x]` euclidean-plane: `EuclideanPlane` so_lambda: `λ2x.t[x]` so_apply: `x[s]` exists: `∃x:A. B[x]`
Lemmas referenced :  euclidean-plane_wf Error :eu-cong-angle_wf,  exists_wf eu-point_wf equal_wf not_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut sqequalRule productEquality lemma_by_obid sqequalHypSubstitution isectElimination thin setElimination rename because_Cache hypothesis hypothesisEquality lambdaEquality

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c:Point.    (eu-bisect-angle(e;a;b;c)  \mmember{}  \mBbbP{})

Date html generated: 2016_06_16-PM-01_31_42
Last ObjectModification: 2016_06_09-AM-09_02_05

Theory : euclidean!geometry

Home Index