let AS be AffinSpace; :: thesis: for A, K being LINE of st AS is AffinPlane holds
ex a being POINT of st
( a on A & a on K )
let A, K be LINE of ; :: thesis: ( AS is AffinPlane implies ex a being POINT of st
( a on A & a on K ) )
consider X being Subset of such that
A1: ( ( A = [X,1] & X is being_line ) or ( A = [(PDir X),2] & X is being_plane ) ) by Th23;
consider X' being Subset of such that
A2: ( ( K = [X',1] & X' is being_line ) or ( K = [(PDir X'),2] & X' is being_plane ) ) by Th23;
assume A3: AS is AffinPlane ; :: thesis: ex a being POINT of st
( a on A & a on K )

A4: now

assume that
A5: A = [X,1] and
A6: X is being_line ; :: thesis: ex a being POINT of st
( a on A & a on K )

A7: now

assume that
A8: K = [X',1] and
A9: X' is being_line ; :: thesis: ex a being POINT of st
( a on A & a on K )

A10: now

reconsider a = LDir X, b = LDir X' as Element of the Points of (IncProjSp_of AS) by A6, A9, Th20;
X' // X' by A9, AFF_1:55;
then A11: X' '||' X' by A9, AFF_4:40;
assume X // X' ; :: thesis: ex a being Element of the Points of (IncProjSp_of AS) st
( a on A & a on K )
then A12: a = b by A6, A9, Th11;
take a = a; :: thesis: ( a on A & a on K )
X // X by A6, AFF_1:55;
then X '||' X by A6, AFF_4:40;
hence ( a on A & a on K ) by A5, A6, A8, A9, A12, A11, Th28; :: thesis: verum

end;

now

assume not X // X' ; :: thesis: ex a being Element of the Points of (IncProjSp_of AS) st
( a on A & a on K )
then consider x being Element of such that
A13: x in X and
A14: x in X' by A3, A6, A9, AFF_1:72;
reconsider a = x as Element of the Points of (IncProjSp_of AS) by Th20;
take a = a; :: thesis: ( a on A & a on K )
thus ( a on A & a on K ) by A5, A6, A8, A9, A13, A14, Th26; :: thesis: verum

end;

hence ex a being POINT of st
( a on A & a on K ) by A10; :: thesis: verum

end;

now

X // X by A6, AFF_1:55;
then A15: X '||' X by A6, AFF_4:40;
reconsider a = LDir X as Element of the Points of (IncProjSp_of AS) by A6, Th20;
assume that
A16: K = [(PDir X'),2] and
A17: X' is being_plane ; :: thesis: ex a being Element of the Points of (IncProjSp_of AS) st
( a on A & a on K )
take a = a; :: thesis: ( a on A & a on K )
X' = the carrier of AS by A3, A17, Th2;
then X '||' X' by A6, A17, AFF_4:42;
hence ( a on A & a on K ) by A5, A6, A16, A17, A15, Th28, Th29; :: thesis: verum

end;

hence ex a being POINT of st
( a on A & a on K ) by A2, A7; :: thesis: verum

end;

now

assume that
A18: A = [(PDir X),2] and
A19: X is being_plane ; :: thesis: ex a being POINT of st
( a on A & a on K )
A20: X = the carrier of AS by A3, A19, Th2;

A21: now

assume that
A22: K = [X',1] and
A23: X' is being_line ; :: thesis: ex a being POINT of st
( a on A & a on K )
X' // X' by A23, AFF_1:55;
then A24: X' '||' X' by A23, AFF_4:40;
reconsider a = LDir X' as POINT of by A23, Th20;
take a = a; :: thesis: ( a on A & a on K )
X' '||' X by A19, A20, A23, AFF_4:42;
hence ( a on A & a on K ) by A18, A19, A22, A23, A24, Th28, Th29; :: thesis: verum

end;

now

consider a, b, c being POINT of such that
A25: a on A and
b on A and
c on A and
a <> b and
b <> c and
c <> a by Lm3;
assume that
A26: K = [(PDir X'),2] and
A27: X' is being_plane ; :: thesis: ex a being POINT of st
( a on A & a on K )
take a = a; :: thesis: ( a on A & a on K )
thus ( a on A & a on K ) by A3, A18, A19, A26, A27, A25, Th3; :: thesis: verum

end;

hence ex a being POINT of st
( a on A & a on K ) by A2, A21; :: thesis: verum

end;

hence ex a being POINT of st
( a on A & a on K ) by A1, A4; :: thesis: verum