let AS be AffinSpace; 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; 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; ( 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
; ( A // C iff a,b // c,d )
thus
( A // C implies a,b // c,d )
( a,b // c,d implies A // C )proof
assume
A // C
;
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;
verum
end;
A13:
C = Line (c,d)
by A3, A4, A6, Lm6;
assume A14:
a,b // c,d
; A // C
A = Line (a,b)
by A1, A2, A5, Lm6;
hence
A // C
by A5, A6, A14, A13, Th36; verum