let AS be AffinSpace; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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:26;
( 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; :: thesis: verum