Nuprl Lemma : geo-between-trivial

e:EuclideanPlane. ∀[a,b:Point].  B(abb)


Proof




Definitions occuring in Statement :  euclidean-plane: EuclideanPlane geo-between: B(abc) geo-point: Point uall: [x:A]. B[x] all: x:A. B[x]
Definitions unfolded in proof :  all: x:A. B[x] uall: [x:A]. B[x] member: t ∈ T euclidean-plane: EuclideanPlane geo-between: B(abc) and: P ∧ Q not: ¬A implies:  Q false: False subtype_rel: A ⊆B guard: {T} uimplies: supposing a sq_stable: SqStable(P) squash: T

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}[a,b:Point].    B(abb)



Date html generated: 2020_05_20-AM-09_46_24
Last ObjectModification: 2019_11_13-AM-10_45_48

Theory : euclidean!plane!geometry


Home Index