let AS be AffinSpace; :: thesis: for a, b, c, a', b' being Element of st AS is AffinPlane & not LIN a,b,c holds
ex c' being Element of st
( a,c // a',c' & b,c // b',c' )
let a, b, c, a', b' be Element of ; :: thesis: ( AS is AffinPlane & not LIN a,b,c implies ex c' being Element of st
( a,c // a',c' & b,c // b',c' ) )
assume that
A1: AS is AffinPlane and
A2: not LIN a,b,c ; :: thesis: ex c' being Element of st
( a,c // a',c' & b,c // b',c' )
consider C being Subset of such that
A3: ( b in C & c in C ) and
A4: C is being_line by Th11;
consider N being Subset of such that
A5: b' in N and
A6: C // N by A4, AFF_1:63;
A7: N is being_line by A6, AFF_1:50;
consider P being Subset of such that
A8: a in P and
A9: c in P and
A10: P is being_line by Th11;
consider M being Subset of such that
A11: a' in M and
A12: P // M by A10, AFF_1:63;
A13: not M // N

proof

assume M // N ; :: thesis: contradiction
then N // P by A12, AFF_1:58;
then C // P by A6, AFF_1:58;
then b in P by A3, A9, AFF_1:59;
hence contradiction by A2, A8, A9, A10, AFF_1:33; :: thesis: verum

end;

M is being_line by A12, AFF_1:50;
then consider c' being Element of such that
A14: c' in M and
A15: c' in N by A1, A7, A13, AFF_1:72;
A16: b,c // b',c' by A3, A5, A6, A15, AFF_1:53;
a,c // a',c' by A8, A9, A11, A12, A14, AFF_1:53;
hence ex c' being Element of st
( a,c // a',c' & b,c // b',c' ) by A16; :: thesis: verum