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

Line (a,b) c= Line (c,d)

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

assume that

A1: c in Line (a,b) and

A2: d in Line (a,b) and

A3: a <> b ; :: thesis: Line (a,b) c= Line (c,d)

A4: LIN a,b,d by A2, Def2;

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

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Line (a,b) or x in Line (c,d) )

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

then reconsider x9 = x as Element of AS ;

LIN a,b,x9 by A6, Def2;

then LIN c,d,x9 by A3, A5, A4, Th7;

hence x in Line (c,d) by Def2; :: thesis: verum

Line (a,b) c= Line (c,d)

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

assume that

A1: c in Line (a,b) and

A2: d in Line (a,b) and

A3: a <> b ; :: thesis: Line (a,b) c= Line (c,d)

A4: LIN a,b,d by A2, Def2;

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

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Line (a,b) or x in Line (c,d) )

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

then reconsider x9 = x as Element of AS ;

LIN a,b,x9 by A6, Def2;

then LIN c,d,x9 by A3, A5, A4, Th7;

hence x in Line (c,d) by Def2; :: thesis: verum