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

for A, C being being_line Subset of AS st a in A & b in A & c in C & d in C & a <> b & c <> d holds

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

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

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

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

assume that

A1: a in A and

A2: b in A and

A3: c in C and

A4: d in C and

A5: a <> b and

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

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

assume A14: a,b // c,d ; :: thesis: A // C

A = Line (a,b) by A1, A2, A5, Lm6;

hence A // C by A5, A6, A14, A13, Th36; :: thesis: verum

for A, C being being_line Subset of AS st a in A & b in A & c in C & d in C & a <> b & c <> d holds

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

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

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

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

assume that

A1: a in A and

A2: b in A and

A3: c in C and

A4: d in C and

A5: a <> b and

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

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

proof

A13:
C = Line (c,d)
by A3, A4, A6, Lm6;
assume
A // C
; :: thesis: a,b // c,d

then consider p, q, r, s being Element of AS such that

A7: p <> q and

A8: r <> s and

A9: p,q // r,s and

A10: A = Line (p,q) and

A11: C = Line (r,s) by Th36;

p,q // a,b by A1, A2, A7, A10, Th21;

then A12: a,b // r,s by A7, A9, Th4;

r,s // c,d by A3, A4, A8, A11, Th21;

hence a,b // c,d by A8, A12, Th4; :: thesis: verum

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

A7: p <> q and

A8: r <> s and

A9: p,q // r,s and

A10: A = Line (p,q) and

A11: C = Line (r,s) by Th36;

p,q // a,b by A1, A2, A7, A10, Th21;

then A12: a,b // r,s by A7, A9, Th4;

r,s // c,d by A3, A4, A8, A11, Th21;

hence a,b // c,d by A8, A12, Th4; :: thesis: verum

assume A14: a,b // c,d ; :: thesis: A // C

A = Line (a,b) by A1, A2, A5, Lm6;

hence A // C by A5, A6, A14, A13, Th36; :: thesis: verum