let AS be AffinSpace; :: thesis: for a, b, c, d being Element of AS st c in Line (a,b) & a <> b holds

( d in Line (a,b) iff a,b // c,d )

let a, b, c, d be Element of AS; :: thesis: ( c in Line (a,b) & a <> b implies ( d in Line (a,b) iff a,b // c,d ) )

assume that

A1: c in Line (a,b) and

A2: a <> b ; :: thesis: ( d in Line (a,b) iff a,b // c,d )

A3: LIN a,b,c by A1, Def2;

thus ( d in Line (a,b) implies a,b // c,d ) :: thesis: ( a,b // c,d implies d in Line (a,b) )

then LIN a,b,d by A2, A3, Th8;

hence d in Line (a,b) by Def2; :: thesis: verum

( d in Line (a,b) iff a,b // c,d )

let a, b, c, d be Element of AS; :: thesis: ( c in Line (a,b) & a <> b implies ( d in Line (a,b) iff a,b // c,d ) )

assume that

A1: c in Line (a,b) and

A2: a <> b ; :: thesis: ( d in Line (a,b) iff a,b // c,d )

A3: LIN a,b,c by A1, Def2;

thus ( d in Line (a,b) implies a,b // c,d ) :: thesis: ( a,b // c,d implies d in Line (a,b) )

proof

assume
a,b // c,d
; :: thesis: d in Line (a,b)
assume
d in Line (a,b)
; :: thesis: a,b // c,d

then LIN a,b,d by Def2;

hence a,b // c,d by A3, Th9; :: thesis: verum

end;then LIN a,b,d by Def2;

hence a,b // c,d by A3, Th9; :: thesis: verum

then LIN a,b,d by A2, A3, Th8;

hence d in Line (a,b) by Def2; :: thesis: verum