Nuprl Lemma : geo-cong-angle-symmetry
∀e:BasicGeometry. ∀a,b,c,x,y,z:Point.
(xyz ≅a abc ⇒ {zyx ≅a abc ∧ xyz ≅a cba ∧ zyx ≅a cba ∧ abc ≅a xyz ∧ cba ≅a xyz ∧ abc ≅a zyx ∧ cba ≅a zyx})
Proof
Definitions occuring in Statement :
geo-cong-angle: abc ≅a xyz,
basic-geometry: BasicGeometry,
geo-point: Point,
guard: {T},
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q
Definitions unfolded in proof :
all: ∀x:A. B[x],
implies: P ⇒ Q,
geo-cong-angle: abc ≅a xyz,
and: P ∧ Q,
cand: A c∧ B,
member: t ∈ T,
basic-geometry: BasicGeometry,
guard: {T},
uall: ∀[x:A]. B[x],
prop: ℙ,
subtype_rel: A ⊆r B,
uimplies: b supposing a
Latex:
\mforall{}e:BasicGeometry. \mforall{}a,b,c,x,y,z:Point.
(xyz \mcong{}\msuba{} abc
{}\mRightarrow{} \{zyx \mcong{}\msuba{} abc \mwedge{} xyz \mcong{}\msuba{} cba \mwedge{} zyx \mcong{}\msuba{} cba \mwedge{} abc \mcong{}\msuba{} xyz \mwedge{} cba \mcong{}\msuba{} xyz \mwedge{} abc \mcong{}\msuba{} zyx \mwedge{} cba \mcong{}\msuba{} zyx\})
Date html generated:
2020_05_20-AM-09_56_58
Last ObjectModification:
2020_01_14-AM-10_29_29
Theory : euclidean!plane!geometry
Home
Index