let l1, l2, l3 be LINE of (IncProjSp_of real_projective_plane); :: thesis: ( l1,l2,l3 are_concurrent iff # l1, # l2, # l3 are_concurrent )
reconsider l91 = # l1, l92 = # l2, l93 = # l3 as Element of ProjectiveLines real_projective_plane ;
hereby :: thesis: ( # l1, # l2, # l3 are_concurrent implies l1,l2,l3 are_concurrent )
assume l1,l2,l3 are_concurrent ; :: thesis: # l1, # l2, # l3 are_concurrent
then # l91, # l92, # l93 are_concurrent ;
hence # l1, # l2, # l3 are_concurrent by Th49; :: thesis: verum
end;
assume # l1, # l2, # l3 are_concurrent ; :: thesis: l1,l2,l3 are_concurrent
then # (# l1), # (# l2), # (# l3) are_concurrent by Th49;
hence l1,l2,l3 are_concurrent ; :: thesis: verum