theorem Th20: :: PROJPL_1:20

for G being IncProjStr
for a, b, c, d being POINT of G
for P, Q, R being LINE of G st a,b,c,d is_a_quadrangle & {a,b} on P & {a,c} on Q & {a,d} on R holds
P,Q,R are_mutually_distinct