let l1, l2, l3 be Element of ProjectiveLines real_projective_plane; :: thesis: ( l1,l2,l3 are_concurrent iff dual l1, dual l2, dual l3 are_collinear )
hereby :: thesis: ( dual l1, dual l2, dual l3 are_collinear implies l1,l2,l3 are_concurrent )
assume l1,l2,l3 are_concurrent ; :: thesis: dual l1, dual l2, dual l3 are_collinear
then dual (dual l1),l2,l3 are_concurrent by Th46;
then dual (dual l1), dual (dual l2),l3 are_concurrent by Th46;
then dual (dual l1), dual (dual l2), dual (dual l3) are_concurrent by Th46;
hence dual l1, dual l2, dual l3 are_collinear by Th59; :: thesis: verum
end;
assume dual l1, dual l2, dual l3 are_collinear ; :: thesis: l1,l2,l3 are_concurrent
then dual (dual l1), dual (dual l2), dual (dual l3) are_concurrent by Th59;
then l1, dual (dual l2), dual (dual l3) are_concurrent by Th46;
then l1,l2, dual (dual l3) are_concurrent by Th46;
hence l1,l2,l3 are_concurrent by Th46; :: thesis: verum