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

A1: now

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

A4: now

given X' being Subset of such that A5: b = LDir X' and
A6: X' is being_line ; :: thesis: ex A being LINE of st
( a on A & b on A )
consider x, y being Element of such that
A7: x in X' and
y in X' and
x <> y by A6, AFF_1:31;
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 such that
A9: X' c= Z and
A10: x * X c= Z and
A11: Z is being_plane by A6, A7, A8, AFF_4:38;
A12: X' '||' Z by A6, A9, A11, AFF_4:42;
reconsider A = [(PDir Z),2] as LINE of 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

assume b is Element of ; :: thesis: ex A being LINE of st
( a on A & b on A )
then reconsider y = b as Element of ;
A13: y * X is being_line by A3, AFF_4:27;
then reconsider A = [(y * X),1] as LINE of 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 st
( a on A & b on A ) by A4, Th20; :: thesis: verum

end;

now

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

A14: now

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

end;

now

assume b is Element of ; :: thesis: ex A being LINE of st
( a on A & b on A )
then reconsider y = b as Element of ;
consider Y being Subset of 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 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 st
( a on A & b on A ) by A14, Th20; :: thesis: verum

end;

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