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

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

a,b // c,d

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

a,b // c,d

let A, C be Subset of AS; :: thesis: ( a in A & b in A & c in C & d in C & A // C implies 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 // C ; :: thesis: a,b // c,d

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

a,b // c,d

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

a,b // c,d

let A, C be Subset of AS; :: thesis: ( a in A & b in A & c in C & d in C & A // C implies 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 // C ; :: thesis: a,b // c,d

now :: thesis: ( a <> b & c <> d implies a,b // c,d )

hence
a,b // c,d
by Th2; :: thesis: verumA6:
C is being_line
by A5, Th35;

assume that

A7: a <> b and

A8: c <> d ; :: thesis: a,b // c,d

A is being_line by A5;

hence a,b // c,d by A1, A2, A3, A4, A5, A7, A8, A6, Th37; :: thesis: verum

end;assume that

A7: a <> b and

A8: c <> d ; :: thesis: a,b // c,d

A is being_line by A5;

hence a,b // c,d by A1, A2, A3, A4, A5, A7, A8, A6, Th37; :: thesis: verum