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: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; :: thesis: verum

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: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; :: thesis: verum