let P, Q, R be Point of real_projective_plane; :: thesis: ( P,Q,R are_collinear iff dual P, dual Q, dual R are_concurrent )
thus ( P,Q,R are_collinear implies dual P, dual Q, dual R are_concurrent ) by Th56; :: thesis: ( dual P, dual Q, dual R are_concurrent implies P,Q,R are_collinear )
assume dual P, dual Q, dual R are_concurrent ; :: thesis: P,Q,R are_collinear
then dual (dual P), dual (dual Q), dual (dual R) are_collinear by Th58;
then P, dual (dual Q), dual (dual R) are_collinear by Th45;
then P,Q, dual (dual R) are_collinear by Th45;
hence P,Q,R are_collinear by Th45; :: thesis: verum