let AS be AffinSpace; for a, b, c, d being Element of AS
for X being Subset of AS st X is being_plane & a in X & b in X & c in X & a,b // c,d & a <> b holds
d in X
let a, b, c, d be Element of AS; for X being Subset of AS st X is being_plane & a in X & b in X & c in X & a,b // c,d & a <> b holds
d in X
let X be Subset of AS; ( X is being_plane & a in X & b in X & c in X & a,b // c,d & a <> b implies d in X )
assume that
A1:
( X is being_plane & a in X & b in X & c in X )
and
A2:
a,b // c,d
and
A3:
a <> b
; d in X
set M = Line (a,b);
set N = c * (Line (a,b));
A4:
Line (a,b) is being_line
by A3, AFF_1:def 3;
then A5:
c * (Line (a,b)) c= X
by A1, A3, Th19, Th28;
A6:
( a in Line (a,b) & b in Line (a,b) )
by AFF_1:15;
( c in c * (Line (a,b)) & Line (a,b) // c * (Line (a,b)) )
by A4, Def3;
then
d in c * (Line (a,b))
by A2, A3, A6, Th7;
hence
d in X
by A5; verum