let AS be AffinSpace; :: thesis: for a, b, c, d being Element of AS

for A being Subset of AS st c in A & d in A & A is being_line & c <> d holds

( a,b // A iff a,b // c,d )

let a, b, c, d be Element of AS; :: thesis: for A being Subset of AS st c in A & d in A & A is being_line & c <> d holds

( a,b // A iff a,b // c,d )

let A be Subset of AS; :: thesis: ( c in A & d in A & A is being_line & c <> d implies ( a,b // A iff a,b // c,d ) )

assume that

A1: c in A and

A2: d in A and

A3: A is being_line and

A4: c <> d ; :: thesis: ( a,b // A iff a,b // c,d )

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

A = Line (c,d) by A1, A2, A3, A4, Lm6;

hence a,b // A by A4, A8; :: thesis: verum

for A being Subset of AS st c in A & d in A & A is being_line & c <> d holds

( a,b // A iff a,b // c,d )

let a, b, c, d be Element of AS; :: thesis: for A being Subset of AS st c in A & d in A & A is being_line & c <> d holds

( a,b // A iff a,b // c,d )

let A be Subset of AS; :: thesis: ( c in A & d in A & A is being_line & c <> d implies ( a,b // A iff a,b // c,d ) )

assume that

A1: c in A and

A2: d in A and

A3: A is being_line and

A4: c <> d ; :: thesis: ( a,b // A iff a,b // c,d )

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

proof

assume A8:
a,b // c,d
; :: thesis: a,b // A
assume
a,b // A
; :: thesis: a,b // c,d

then consider p, q being Element of AS such that

A5: p <> q and

A6: A = Line (p,q) and

A7: a,b // p,q ;

p,q // c,d by A1, A2, A5, A6, Th21;

hence a,b // c,d by A5, A7, Th4; :: thesis: verum

end;then consider p, q being Element of AS such that

A5: p <> q and

A6: A = Line (p,q) and

A7: a,b // p,q ;

p,q // c,d by A1, A2, A5, A6, Th21;

hence a,b // c,d by A5, A7, Th4; :: thesis: verum

A = Line (c,d) by A1, A2, A3, A4, Lm6;

hence a,b // A by A4, A8; :: thesis: verum