let AS be AffinSpace; for a, b, c, a9, b9 being Element of AS
for X being Subset of AS st not LIN a,b,c & a,b // a9,b9 & a in X & b in X & c in X & X is being_plane & a9 in X holds
ex c9 being Element of AS st
( a,c // a9,c9 & b,c // b9,c9 )
let a, b, c, a9, b9 be Element of AS; for X being Subset of AS st not LIN a,b,c & a,b // a9,b9 & a in X & b in X & c in X & X is being_plane & a9 in X holds
ex c9 being Element of AS st
( a,c // a9,c9 & b,c // b9,c9 )
let X be Subset of AS; ( not LIN a,b,c & a,b // a9,b9 & a in X & b in X & c in X & X is being_plane & a9 in X implies ex c9 being Element of AS st
( a,c // a9,c9 & b,c // b9,c9 ) )
assume that
A1:
not LIN a,b,c
and
A2:
a,b // a9,b9
and
A3:
a in X
and
A4:
b in X
and
A5:
c in X
and
A6:
X is being_plane
and
A7:
a9 in X
; ex c9 being Element of AS st
( a,c // a9,c9 & b,c // b9,c9 )
set C = Line (b,c);
set P = Line (a,c);
set P9 = a9 * (Line (a,c));
set C9 = b9 * (Line (b,c));
A8:
b <> c
by A1, AFF_1:7;
then A9:
Line (b,c) is being_line
by AFF_1:def 3;
then A10:
Line (b,c) // b9 * (Line (b,c))
by Def3;
a <> b
by A1, AFF_1:7;
then
b9 in X
by A2, A3, A4, A6, A7, Th29;
then A11:
b9 * (Line (b,c)) c= X
by A4, A5, A6, A8, A9, Th19, Th28;
A12:
c in Line (a,c)
by AFF_1:15;
A13:
b9 * (Line (b,c)) is being_line
by A9, Th27;
A14:
a in Line (a,c)
by AFF_1:15;
A15:
c <> a
by A1, AFF_1:7;
then A16:
Line (a,c) is being_line
by AFF_1:def 3;
then A17:
a9 * (Line (a,c)) is being_line
by Th27;
A18:
( b in Line (b,c) & c in Line (b,c) )
by AFF_1:15;
A19:
Line (a,c) // a9 * (Line (a,c))
by A16, Def3;
A20:
not b9 * (Line (b,c)) // a9 * (Line (a,c))
proof
assume
b9 * (Line (b,c)) // a9 * (Line (a,c))
;
contradiction
then
b9 * (Line (b,c)) // Line (
a,
c)
by A19, AFF_1:44;
then
Line (
b,
c)
// Line (
a,
c)
by A10, AFF_1:44;
then
b in Line (
a,
c)
by A12, A18, AFF_1:45;
hence
contradiction
by A1, A14, A12, A16, AFF_1:21;
verum
end;
a9 * (Line (a,c)) c= X
by A3, A5, A6, A7, A15, A16, Th19, Th28;
then consider c9 being Element of AS such that
A21:
c9 in b9 * (Line (b,c))
and
A22:
c9 in a9 * (Line (a,c))
by A6, A17, A13, A20, A11, Th22;
b9 in b9 * (Line (b,c))
by A9, Def3;
then A23:
b,c // b9,c9
by A18, A10, A21, AFF_1:39;
a9 in a9 * (Line (a,c))
by A16, Def3;
then
a,c // a9,c9
by A14, A12, A19, A22, AFF_1:39;
hence
ex c9 being Element of AS st
( a,c // a9,c9 & b,c // b9,c9 )
by A23; verum