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

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 the carrier of AS ;

A2: now

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
A3: ( x in Y & y in Y & Y is being_line ) by AFF_4:11;
reconsider A = [Y,1] as LINE of (IncProjSp_of AS) by A3, Th23;
take A = A; :: thesis: ( a on A & b on A )
thus ( a on A & b on A ) by A3, Th26; :: thesis: verum

end;

now

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

end;

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

end;

now

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

A7: now

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 ;
A8: ( y * X is being_line & y in y * X ) by A6, AFF_4:27, AFF_4:def 3;
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 A6, AFF_4:def 3;
then X '||' y * X by A6, A8, AFF_4:40;
hence a on A by A6, A8, Th28; :: thesis: b on A
thus b on A by A8, Th26; :: thesis: verum

end;

now

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

end;

hence ex A being LINE of (IncProjSp_of AS) st
( a on A & b on A ) by A7, 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