let AS be AffinSpace; 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; ( 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)
; ( 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 ( A = M implies ex q being Element of AS st
( q in P & q in Q ) )assume
A = M
;
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;
verum end;
A // M
by A11, A17, AFF_1:44;
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; verum