let AS be AffinSpace; 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; 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; ( 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
; a,b // c,d
now ( a <> b & c <> d implies a,b // c,d )A6:
C is
being_line
by A5, Th35;
assume that A7:
a <> b
and A8:
c <> d
;
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;
verum end;
hence
a,b // c,d
by Th2; verum