let AS be AffinSpace; for A, P, C being Subset of AS
for o, a, b, c, a9, b9, c9 being Element of AS st o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 & ( o = a9 or a = a9 ) holds
b,c // b9,c9
let A, P, C be Subset of AS; for o, a, b, c, a9, b9, c9 being Element of AS st o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 & ( o = a9 or a = a9 ) holds
b,c // b9,c9
let o, a, b, c, a9, b9, c9 be Element of AS; ( o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 & ( o = a9 or a = a9 ) implies b,c // b9,c9 )
assume that
A1:
o in A
and
A2:
o in P
and
A3:
o in C
and
A4:
o <> a
and
A5:
o <> b
and
A6:
o <> c
and
A7:
a in A
and
A8:
b in P
and
A9:
b9 in P
and
A10:
c in C
and
A11:
c9 in C
and
A12:
A is being_line
and
A13:
P is being_line
and
A14:
C is being_line
and
A15:
A <> P
and
A16:
A <> C
and
A17:
a,b // a9,b9
and
A18:
a,c // a9,c9
and
A19:
( o = a9 or a = a9 )
; b,c // b9,c9
A20:
now ( a = a9 implies b,c // b9,c9 )assume A21:
a = a9
;
b,c // b9,c9then A22:
c = c9
by A1, A3, A4, A6, A7, A10, A11, A12, A14, A16, A18, AFF_4:9;
b = b9
by A1, A2, A4, A5, A7, A8, A9, A12, A13, A15, A17, A21, AFF_4:9;
hence
b,
c // b9,
c9
by A22, AFF_1:2;
verum end;
now ( o = a9 implies b,c // b9,c9 )assume A23:
o = a9
;
b,c // b9,c9then A24:
o = c9
by A1, A3, A4, A6, A7, A10, A11, A12, A14, A16, A18, AFF_4:8;
o = b9
by A1, A2, A4, A5, A7, A8, A9, A12, A13, A15, A17, A23, AFF_4:8;
hence
b,
c // b9,
c9
by A24, AFF_1:3;
verum end;
hence
b,c // b9,c9
by A19, A20; verum