let P be Element of absolute ; :: thesis: P in tangent P
ex p being Element of real_projective_plane st
( p = P & tangent P = Line (p,(pole_infty P)) ) by Def04;
hence P in tangent P by COLLSP:10; :: thesis: verum