let AS be AffinSpace; for a, b, c, d being Element of AS
for A, C being Subset of AS st A is being_line & C is being_line & 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 Subset of AS st A is being_line & C is being_line & 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 Subset of AS; ( A is being_line & C is being_line & 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 is being_line
and
A2:
C is being_line
and
A3:
a in A
and
A4:
b in A
and
A5:
c in C
and
A6:
d in C
and
A7:
a <> b
and
A8:
c <> d
; ( A // C iff a,b // c,d )
A9:
( A // C implies a,b // c,d )
proof
assume
A // C
;
a,b // c,d
then consider p,
q,
r,
s being
Element of
AS such that A10:
p <> q
and A11:
r <> s
and A12:
p,
q // r,
s
and A13:
A = Line p,
q
and A14:
C = Line r,
s
by Th51;
p,
q // a,
b
by A3, A4, A10, A13, Th36;
then A15:
a,
b // r,
s
by A10, A12, Th14;
r,
s // c,
d
by A5, A6, A11, A14, Th36;
hence
a,
b // c,
d
by A11, A15, Th14;
verum
end;
( a,b // c,d implies A // C )
proof
A16:
C = Line c,
d
by A2, A5, A6, A8, Lm6;
assume A17:
a,
b // c,
d
;
A // C
A = Line a,
b
by A1, A3, A4, A7, Lm6;
hence
A // C
by A7, A8, A17, A16, Th51;
verum
end;
hence
( A // C iff a,b // c,d )
by A9; verum