let L be LINE of (IncProjSp_of real_projective_plane); :: thesis: for P, Q being Element of (ProjectiveSpace (TOP-REAL 3)) st P <> Q & P in L & Q in L holds
L = Line (P,Q)
let P, Q be Element of (ProjectiveSpace (TOP-REAL 3)); :: thesis: ( P <> Q & P in L & Q in L implies L = Line (P,Q) )
assume that
A1: P <> Q and
A2: P in L and
A3: Q in L ; :: thesis: L = Line (P,Q)
reconsider L9 = L as LINE of real_projective_plane by INCPROJ:4;
L9 = Line (P,Q) by A1, A2, A3, COLLSP:19;
hence L = Line (P,Q) ; :: thesis: verum