let AS be AffinSpace; :: thesis: for a, a', b, b', c, c' being Element of AS
for A, P, C being Subset of AS st AS is not AffinPlane & A // P & A // C & a in A & a' in A & b in P & b' in P & c in C & c' in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a',b' & a,c // a',c' holds
b,c // b',c'
let a, a', b, b', c, c' be Element of AS; :: thesis: for A, P, C being Subset of AS st AS is not AffinPlane & A // P & A // C & a in A & a' in A & b in P & b' in P & c in C & c' in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a',b' & a,c // a',c' holds
b,c // b',c'
let A, P, C be Subset of AS; :: thesis: ( AS is not AffinPlane & A // P & A // C & a in A & a' in A & b in P & b' in P & c in C & c' in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a',b' & a,c // a',c' implies b,c // b',c' )
assume that
A1: AS is not AffinPlane and
A2: ( A // P & A // C ) and
A3: ( a in A & a' in A & b in P & b' in P & c in C & c' in C ) and
A4: ( A is being_line & P is being_line & C is being_line ) and
A5: ( A <> P & A <> C ) and
A6: ( a,b // a',b' & a,c // a',c' ) ; :: thesis: b,c // b',c'

now

assume A,P,C is_coplanar ; :: thesis: b,c // b',c'
then consider X being Subset of AS such that
A7: ( A c= X & P c= X & C c= X ) and
A8: X is being_plane by Def5;
consider d being Element of AS such that
A9: not d in X by A1, A8, Th48;
set K = d * A;
A10: ( d in d * A & A // d * A ) by A4, Def3;
then A11: ( d * A // P & d * A // C ) by A2, AFF_1:58;
A12: d * A is being_line by A4, Th27;
A13: not d * A c= X by A9, A10;
ex d' being Element of AS st
( d' in d * A & a,d // a',d' )

proof

A14: now

assume A15: a <> a' ; :: thesis: ex d' being Element of AS st
( d' in d * A & a,d // a',d' )
consider d' being Element of AS such that
A16: a,a' // d,d' and
A17: a,d // a',d' by DIRAF:47;
d,d' // a,a' by A16, AFF_1:13;
then d,d' // A by A3, A4, A15, AFF_1:41;
then d,d' // d * A by A10, Th3;
then d' in d * A by A10, Th2;
hence ex d' being Element of AS st
( d' in d * A & a,d // a',d' ) by A17; :: thesis: verum

end;

now

assume A18: a = a' ; :: thesis: ex d' being Element of AS st
( d' in d * A & a,d // a',d' )
take d' = d; :: thesis: ( d' in d * A & a,d // a',d' )
thus d' in d * A by A4, Def3; :: thesis: a,d // a',d'
thus a,d // a',d' by A18, AFF_1:11; :: thesis: verum

end;

hence ex d' being Element of AS st
( d' in d * A & a,d // a',d' ) by A14; :: thesis: verum

end;

then consider d' being Element of AS such that
A19: d' in d * A and
A20: a,d // a',d' ;

now

assume A21: P <> C ; :: thesis: b,c // b',c'
A22: d * A <> A by A7, A9, A10;
A23: d * A <> P by A7, A9, A10;
A24: d * A <> C by A7, A9, A10;
A25: not A,d * A,C is_coplanar

proof

assume A,d * A,C is_coplanar ; :: thesis: contradiction
then A,C,d * A is_coplanar by Th44;
hence contradiction by A4, A5, A7, A8, A13, Th46; :: thesis: verum

end;

A26: not A,d * A,P is_coplanar

proof

assume A,d * A,P is_coplanar ; :: thesis: contradiction
then A,P,d * A is_coplanar by Th44;
hence contradiction by A4, A5, A7, A8, A13, Th46; :: thesis: verum

end;

A27: not d * A,P,C is_coplanar

proof

assume d * A,P,C is_coplanar ; :: thesis: contradiction
then P,C,d * A is_coplanar by Th44;
hence contradiction by A4, A7, A8, A13, A21, Th46; :: thesis: verum

end;

A28: d,c // d',c' by A2, A3, A4, A5, A6, A10, A12, A19, A20, A22, A25, Lm11;
d,b // d',b' by A2, A3, A4, A5, A6, A10, A12, A19, A20, A22, A26, Lm11;
hence b,c // b',c' by A3, A4, A10, A11, A12, A19, A23, A24, A27, A28, Lm11; :: thesis: verum

end;

hence b,c // b',c' by A3, A4, AFF_1:65; :: thesis: verum

end;

hence b,c // b',c' by A2, A3, A4, A5, A6, Lm11; :: thesis: verum