Nuprl Lemma : geo-sas2
∀e:BasicGeometry. ∀a,b,c,A,B,C:Point. bc ≅ BC supposing (ab ≅ AB ∧ ac ≅ AC) ∧ bac ≅a BAC
Proof
Definitions occuring in Statement :
geo-cong-angle: abc ≅a xyz,
basic-geometry: BasicGeometry,
geo-congruent: ab ≅ cd,
geo-point: Point,
uimplies: b supposing a,
all: ∀x:A. B[x],
and: P ∧ Q
Definitions unfolded in proof :
all: ∀x:A. B[x],
uimplies: b supposing a,
member: t ∈ T,
and: P ∧ Q,
geo-cong-angle: abc ≅a xyz,
exists: ∃x:A. B[x],
basic-geometry: BasicGeometry,
implies: P ⇒ Q,
uall: ∀[x:A]. B[x],
cand: A c∧ B,
subtype_rel: A ⊆r B,
prop: ℙ,
guard: {T},
geo-congruent: ab ≅ cd,
not: ¬A,
false: False
Latex:
\mforall{}e:BasicGeometry. \mforall{}a,b,c,A,B,C:Point. bc \mcong{} BC supposing (ab \mcong{} AB \mwedge{} ac \mcong{} AC) \mwedge{} bac \mcong{}\msuba{} BAC
Date html generated:
2020_05_20-AM-09_58_50
Last ObjectModification:
2019_12_26-PM-08_32_27
Theory : euclidean!plane!geometry
Home
Index