let AS be AffinSpace; for A, C being Subset of AS holds
( A // C iff ex a, b, c, d being Element of AS st
( a <> b & c <> d & a,b // c,d & A = Line (a,b) & C = Line (c,d) ) )
let A, C be Subset of AS; ( A // C iff ex a, b, c, d being Element of AS st
( a <> b & c <> d & a,b // c,d & A = Line (a,b) & C = Line (c,d) ) )
thus
( A // C implies ex a, b, c, d being Element of AS st
( a <> b & c <> d & a,b // c,d & A = Line (a,b) & C = Line (c,d) ) )
( ex a, b, c, d being Element of AS st
( a <> b & c <> d & a,b // c,d & A = Line (a,b) & C = Line (c,d) ) implies A // C )proof
assume
A // C
;
ex a, b, c, d being Element of AS st
( a <> b & c <> d & a,b // c,d & A = Line (a,b) & C = Line (c,d) )
then consider a,
b being
Element of
AS such that A1:
A = Line (
a,
b)
and A2:
a <> b
and A3:
a,
b // C
;
ex
c,
d being
Element of
AS st
(
c <> d &
C = Line (
c,
d) &
a,
b // c,
d )
by A3;
hence
ex
a,
b,
c,
d being
Element of
AS st
(
a <> b &
c <> d &
a,
b // c,
d &
A = Line (
a,
b) &
C = Line (
c,
d) )
by A1, A2;
verum
end;
given a, b, c, d being Element of AS such that A4:
a <> b
and
A5:
c <> d
and
A6:
a,b // c,d
and
A7:
A = Line (a,b)
and
A8:
C = Line (c,d)
; A // C
a,b // C
by A5, A6, A8;
hence
A // C
by A4, A7; verum