let AS be AffinSpace; :: thesis: for a, a', b, b', c, c' being Element of
for A, P, C being Subset of 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 ; :: thesis: for A, P, C being Subset of 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 ; :: 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 and
A3: A // C and
A4: ( a in A & a' in A ) and
A5: ( b in P & b' in P ) and
A6: ( c in C & c' in C ) and
A7: A is being_line and
A8: P is being_line and
A9: C is being_line and
A10: A <> P and
A11: A <> C and
A12: a,b // a',b' and
A13: 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 such that
A14: A c= X and
A15: P c= X and
A16: C c= X and
A17: X is being_plane by Def5;
consider d being Element of such that
A18: not d in X by A1, A17, Th48;
set K = d * A;
A19: d in d * A by A7, Def3;
then A20: not d * A c= X by A18;
A21: A // d * A by A7, Def3;
ex d' being Element of st
( d' in d * A & a,d // a',d' )

proof

A22: now

assume A23: a <> a' ; :: thesis: ex d' being Element of st
( d' in d * A & a,d // a',d' )
consider d' being Element of such that
A24: a,a' // d,d' and
A25: a,d // a',d' by DIRAF:47;
d,d' // a,a' by A24, AFF_1:13;
then d,d' // A by A4, A7, A23, AFF_1:41;
then d,d' // d * A by A21, Th3;
then d' in d * A by A19, Th2;
hence ex d' being Element of st
( d' in d * A & a,d // a',d' ) by A25; :: thesis: verum

end;

now

assume A26: a = a' ; :: thesis: ex d' being Element of 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 A7, Def3; :: thesis: a,d // a',d'
thus a,d // a',d' by A26, AFF_1:11; :: thesis: verum

end;

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

end;

then consider d' being Element of such that
A27: d' in d * A and
A28: a,d // a',d' ;
A29: ( d * A // P & d * A // C ) by A2, A3, A21, AFF_1:58;

now

assume A30: P <> C ; :: thesis: b,c // b',c'
A31: 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 A8, A9, A15, A16, A17, A20, A30, Th46; :: thesis: verum

end;

A32: d * A <> A by A14, A18, A19;
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 A7, A8, A10, A14, A15, A17, A20, Th46; :: thesis: verum

end;

then A33: d,b // d',b' by A2, A4, A5, A7, A10, A12, A19, A21, A27, A28, A32, Lm11;
A34: ( d * A <> P & d * A <> C ) by A15, A16, A18, A19;
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 A7, A9, A11, A14, A16, A17, A20, Th46; :: thesis: verum

end;

then d,c // d',c' by A3, A4, A6, A7, A11, A13, A19, A21, A27, A28, A32, Lm11;
hence b,c // b',c' by A5, A6, A7, A19, A29, A27, A34, A31, A33, Lm11, Th27; :: thesis: verum

end;

hence b,c // b',c' by A5, A6, A8, AFF_1:65; :: thesis: verum

end;

hence b,c // b',c' by A2, A3, A4, A5, A6, A7, A10, A11, A12, A13, Lm11; :: thesis: verum