let AS be AffinSpace; :: thesis: for a, b being POINT of (IncProjSp_of AS) ex A being LINE of (IncProjSp_of AS) st
( a on A & b on A )
let a, b be POINT of (IncProjSp_of AS); :: thesis: ex A being LINE of (IncProjSp_of AS) st
( a on A & b on A )

A1: now :: thesis: ( ex X being Subset of AS st
( a = LDir X & X is being_line ) implies ex A being LINE of (IncProjSp_of AS) st
( a on A & b on A ) )

given X being Subset of AS such that A2: a = LDir X and
A3: X is being_line ; :: thesis: ex A being LINE of (IncProjSp_of AS) st
( a on A & b on A )

A4: now :: thesis: ( ex X9 being Subset of AS st
( b = LDir X9 & X9 is being_line ) implies ex A being LINE of (IncProjSp_of AS) st
( a on A & b on A ) )

given X9 being Subset of AS such that A5: b = LDir X9 and
A6: X9 is being_line ; :: thesis: ex A being LINE of (IncProjSp_of AS) st
( a on A & b on A )
consider x, y being Element of AS such that
A7: x in X9 and
y in X9 and
x <> y by A6, AFF_1:19;
A8: x in x * X by A3, AFF_4:def 3;
x * X is being_line by A3, AFF_4:27;
then consider Z being Subset of AS such that
A9: X9 c= Z and
A10: x * X c= Z and
A11: Z is being_plane by A6, A7, A8, AFF_4:38;
A12: X9 '||' Z by A6, A9, A11, AFF_4:42;
reconsider A = [(PDir Z),2] as LINE of (IncProjSp_of AS) by A11, Th23;
take A = A; :: thesis: ( a on A & b on A )
X // x * X by A3, AFF_4:def 3;
then X '||' Z by A3, A10, A11, AFF_4:41;
hence ( a on A & b on A ) by A2, A3, A5, A6, A11, A12, Th29; :: thesis: verum

end;

now :: thesis: ( b is Element of AS implies ex A being LINE of (IncProjSp_of AS) st
( a on A & b on A ) )

assume b is Element of AS ; :: thesis: ex A being LINE of (IncProjSp_of AS) st
( a on A & b on A )
then reconsider y = b as Element of AS ;
A13: y * X is being_line by A3, AFF_4:27;
then reconsider A = [(y * X),1] as LINE of (IncProjSp_of AS) by Th23;
take A = A; :: thesis: ( a on A & b on A )
X // y * X by A3, AFF_4:def 3;
then X '||' y * X by A3, A13, AFF_4:40;
hence a on A by A2, A3, A13, Th28; :: thesis: b on A
y in y * X by A3, AFF_4:def 3;
hence b on A by A13, Th26; :: thesis: verum

end;

hence ex A being LINE of (IncProjSp_of AS) st
( a on A & b on A ) by A4, Th20; :: thesis: verum

end;

now :: thesis: ( a is Element of AS implies ex A being LINE of (IncProjSp_of AS) st
( a on A & b on A ) )

assume a is Element of AS ; :: thesis: ex A being LINE of (IncProjSp_of AS) st
( a on A & b on A )
then reconsider x = a as Element of AS ;

A14: now :: thesis: ( ex X9 being Subset of AS st
( b = LDir X9 & X9 is being_line ) implies ex A being LINE of (IncProjSp_of AS) st
( a on A & b on A ) )

given X9 being Subset of AS such that A15: b = LDir X9 and
A16: X9 is being_line ; :: thesis: ex A being LINE of (IncProjSp_of AS) st
( a on A & b on A )
A17: x * X9 is being_line by A16, AFF_4:27;
then reconsider A = [(x * X9),1] as LINE of (IncProjSp_of AS) by Th23;
take A = A; :: thesis: ( a on A & b on A )
x in x * X9 by A16, AFF_4:def 3;
hence a on A by A17, Th26; :: thesis: b on A
X9 // x * X9 by A16, AFF_4:def 3;
then X9 '||' x * X9 by A16, A17, AFF_4:40;
hence b on A by A15, A16, A17, Th28; :: thesis: verum

end;

now :: thesis: ( b is Element of AS implies ex A being LINE of (IncProjSp_of AS) st
( a on A & b on A ) )

assume b is Element of AS ; :: thesis: ex A being LINE of (IncProjSp_of AS) st
( a on A & b on A )
then reconsider y = b as Element of AS ;
consider Y being Subset of AS such that
A18: x in Y and
A19: y in Y and
A20: Y is being_line by AFF_4:11;
reconsider A = [Y,1] as LINE of (IncProjSp_of AS) by A20, Th23;
take A = A; :: thesis: ( a on A & b on A )
thus ( a on A & b on A ) by A18, A19, A20, Th26; :: thesis: verum

end;

hence ex A being LINE of (IncProjSp_of AS) st
( a on A & b on A ) by A14, Th20; :: thesis: verum

end;

hence ex A being LINE of (IncProjSp_of AS) st
( a on A & b on A ) by A1, Th20; :: thesis: verum