let P, Q be Point of BK-model-Plane; :: thesis: ( P <> Q implies ( length (P,P,Q) = 0 & length (P,Q,Q) = 1 ) )
assume A1: P <> Q ; :: thesis: ( length (P,P,Q) = 0 & length (P,Q,Q) = 1 )
reconsider P2 = BK_to_T2 P, Q2 = BK_to_T2 Q as Point of TarskiEuclid2Space ;
A2: between P,P,Q by Th09;
A3: between P,Q,Q by Th09;
reconsider r = 0 as Real ;
now :: thesis: ( 0 <= r & r <= 1 & ((1 - r) * (Tn2TR (BK_to_T2 P))) + (r * (Tn2TR (BK_to_T2 Q))) = Tn2TR (BK_to_T2 P) )
thus ( 0 <= r & r <= 1 ) ; :: thesis: ((1 - r) * (Tn2TR (BK_to_T2 P))) + (r * (Tn2TR (BK_to_T2 Q))) = Tn2TR (BK_to_T2 P)
thus ((1 - r) * (Tn2TR (BK_to_T2 P))) + (r * (Tn2TR (BK_to_T2 Q))) = |[(1 * ((Tn2TR (BK_to_T2 P)) `1)),(1 * ((Tn2TR (BK_to_T2 P)) `2))]| + (0 * (Tn2TR (BK_to_T2 Q))) by EUCLID:57
.= |[((Tn2TR (BK_to_T2 P)) `1),((Tn2TR (BK_to_T2 P)) `2)]| + |[(0 * ((Tn2TR (BK_to_T2 Q)) `1)),(0 * ((Tn2TR (BK_to_T2 Q)) `2))]| by EUCLID:57
.= |[(((Tn2TR (BK_to_T2 P)) `1) + 0),(((Tn2TR (BK_to_T2 P)) `2) + 0)]| by EUCLID:56
.= Tn2TR (BK_to_T2 P) by EUCLID:53 ; :: thesis: verum
end;
hence length (P,P,Q) = 0 by A1, A2, Def03; :: thesis: length (P,Q,Q) = 1
reconsider s = 1 as Real ;
now :: thesis: ( 0 <= s & s <= 1 & ((1 - s) * (Tn2TR (BK_to_T2 P))) + (s * (Tn2TR (BK_to_T2 Q))) = Tn2TR (BK_to_T2 Q) )
thus ( 0 <= s & s <= 1 ) ; :: thesis: ((1 - s) * (Tn2TR (BK_to_T2 P))) + (s * (Tn2TR (BK_to_T2 Q))) = Tn2TR (BK_to_T2 Q)
thus ((1 - s) * (Tn2TR (BK_to_T2 P))) + (s * (Tn2TR (BK_to_T2 Q))) = |[(1 * ((Tn2TR (BK_to_T2 Q)) `1)),(1 * ((Tn2TR (BK_to_T2 Q)) `2))]| + (0 * (Tn2TR (BK_to_T2 P))) by EUCLID:57
.= |[((Tn2TR (BK_to_T2 Q)) `1),((Tn2TR (BK_to_T2 Q)) `2)]| + |[(0 * ((Tn2TR (BK_to_T2 P)) `1)),(0 * ((Tn2TR (BK_to_T2 P)) `2))]| by EUCLID:57
.= |[(((Tn2TR (BK_to_T2 Q)) `1) + 0),(((Tn2TR (BK_to_T2 Q)) `2) + 0)]| by EUCLID:56
.= Tn2TR (BK_to_T2 Q) by EUCLID:53 ; :: thesis: verum
end;
hence length (P,Q,Q) = 1 by A1, A3, Def03; :: thesis: verum