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