[e:EuclideanPlane]. ∀[x,y:{p:Point| O_X_p} ].  (x x ∈ {p:Point| O_X_p} )

Proof

Definitions occuring in Statement :  eu-add-length: q euclidean-plane: EuclideanPlane eu-between-eq: a_b_c eu-X: X eu-O: O eu-point: Point uall: [x:A]. B[x] set: {x:A| B[x]}  equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T euclidean-plane: EuclideanPlane all: x:A. B[x] prop: so_lambda: λ2x.t[x] so_apply: x[s] eu-add-length: q and: P ∧ Q not: ¬A implies:  Q uimplies: supposing a false: False stable: Stable{P} uiff: uiff(P;Q) sq_stable: SqStable(P) squash: T
Lemmas referenced :  eu-between-eq_wf eu-O_wf eu-X_wf set_wf eu-point_wf eu-not-colinear-OXY eu-between-eq-same equal_wf eu-extend-property not_wf eu-extend_wf eu-congruent_wf eu-between-eq-symmetry eu-between-eq-inner-trans eu-between-eq-exchange3 eu-between-eq-exchange4 eu-construction-unicity stable__eu-congruent eu-congruence-identity eu-congruent-iff-length eu-length-flip eu-three-segment eu-add-length_wf sq_stable__eu-between-eq
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut dependent_set_memberEquality extract_by_obid sqequalHypSubstitution isectElimination thin setElimination rename because_Cache hypothesis dependent_functionElimination hypothesisEquality sqequalRule lambdaEquality isect_memberEquality axiomEquality productElimination lambdaFormation equalitySymmetry hyp_replacement Error :applyLambdaEquality,  equalityTransitivity independent_isectElimination independent_functionElimination voidElimination productEquality equalityEquality promote_hyp imageMemberEquality baseClosed imageElimination

Latex:
\mforall{}[e:EuclideanPlane].  \mforall{}[x,y:\{p:Point|  O\_X\_p\}  ].    (x  +  y  =  y  +  x)

Date html generated: 2016_10_26-AM-07_41_54
Last ObjectModification: 2016_07_12-AM-08_08_14

Theory : euclidean!geometry

Home Index