let AS be AffinSpace; :: thesis: for K, P, Q being Subset of AS st K is being_line & P is being_line & Q is being_line & Q c= Plane (K,P) & not P // Q holds

ex q being Element of AS st

( q in P & q in Q )

let K, P, Q be Subset of AS; :: thesis: ( K is being_line & P is being_line & Q is being_line & Q c= Plane (K,P) & not P // Q implies ex q being Element of AS st

( q in P & q in Q ) )

assume that

A1: K is being_line and

A2: P is being_line and

A3: Q is being_line and

A4: Q c= Plane (K,P) ; :: thesis: ( P // Q or ex q being Element of AS st

( q in P & q in Q ) )

consider a, b being Element of AS such that

A5: a in Q and

A6: b in Q and

A7: a <> b by A3, AFF_1:19;

consider a9 being Element of AS such that

A8: a,a9 // K and

A9: a9 in P by A4, A5, Lm3;

consider A being Subset of AS such that

A10: a9 in A and

A11: K // A by A1, AFF_1:49;

A12: a9,a // A by A8, A11, Th3;

then A13: a in A by A10, Th2;

consider b9 being Element of AS such that

A14: b,b9 // K and

A15: b9 in P by A4, A6, Lm3;

consider M being Subset of AS such that

A16: b9 in M and

A17: K // M by A1, AFF_1:49;

A18: b9,b // M by A14, A17, Th3;

then A19: b in M by A16, Th2;

A20: A is being_line by A11, AFF_1:36;

hence ( P // Q or ex q being Element of AS st

( q in P & q in Q ) ) by A2, A3, A5, A6, A9, A15, A10, A16, A13, A19, A21, Th18; :: thesis: verum

ex q being Element of AS st

( q in P & q in Q )

let K, P, Q be Subset of AS; :: thesis: ( K is being_line & P is being_line & Q is being_line & Q c= Plane (K,P) & not P // Q implies ex q being Element of AS st

( q in P & q in Q ) )

assume that

A1: K is being_line and

A2: P is being_line and

A3: Q is being_line and

A4: Q c= Plane (K,P) ; :: thesis: ( P // Q or ex q being Element of AS st

( q in P & q in Q ) )

consider a, b being Element of AS such that

A5: a in Q and

A6: b in Q and

A7: a <> b by A3, AFF_1:19;

consider a9 being Element of AS such that

A8: a,a9 // K and

A9: a9 in P by A4, A5, Lm3;

consider A being Subset of AS such that

A10: a9 in A and

A11: K // A by A1, AFF_1:49;

A12: a9,a // A by A8, A11, Th3;

then A13: a in A by A10, Th2;

consider b9 being Element of AS such that

A14: b,b9 // K and

A15: b9 in P by A4, A6, Lm3;

consider M being Subset of AS such that

A16: b9 in M and

A17: K // M by A1, AFF_1:49;

A18: b9,b // M by A14, A17, Th3;

then A19: b in M by A16, Th2;

A20: A is being_line by A11, AFF_1:36;

A21: now :: thesis: ( A = M implies ex q being Element of AS st

( q in P & q in Q ) )

A // M
by A11, A17, AFF_1:44;( q in P & q in Q ) )

assume
A = M
; :: thesis: ex q being Element of AS st

( q in P & q in Q )

then A22: b in A by A16, A18, Th2;

a in A by A10, A12, Th2;

then a9 in Q by A3, A5, A6, A7, A10, A20, A22, AFF_1:18;

hence ex q being Element of AS st

( q in P & q in Q ) by A9; :: thesis: verum

end;( q in P & q in Q )

then A22: b in A by A16, A18, Th2;

a in A by A10, A12, Th2;

then a9 in Q by A3, A5, A6, A7, A10, A20, A22, AFF_1:18;

hence ex q being Element of AS st

( q in P & q in Q ) by A9; :: thesis: verum

hence ( P // Q or ex q being Element of AS st

( q in P & q in Q ) ) by A2, A3, A5, A6, A9, A15, A10, A16, A13, A19, A21, Th18; :: thesis: verum