let AS be AffinSpace; :: thesis: for a, b, c, a', b' being Element of st not LIN a,b,c & a' <> b' & a,b // a',b' 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: ( not LIN a,b,c & a' <> b' & a,b // a',b' implies ex c' being Element of st
( a,c // a',c' & b,c // b',c' ) )
assume that
A1: not LIN a,b,c and
A2: a' <> b' and
A3: a,b // a',b' ; :: thesis: ex c' being Element of st
( a,c // a',c' & b,c // b',c' )

now

consider X being Subset of such that
A4: a in X and
A5: b in X and
A6: c in X and
A7: X is being_plane by Th37;
assume A8: AS is not AffinPlane ; :: thesis: ex c' being Element of st
( a,c // a',c' & b,c // b',c' )

now

set A = Line a,a';
set P = Line b,b';
set AB = Line a,b;
set AB' = Line a',b';
A9: a in Line a,b by AFF_1:26;
assume A10: not a' in X ; :: thesis: ex c' being Element of st
( a,c // a',c' & b,c // b',c' )
then A11: Line a,a' is being_line by A4, AFF_1:def 3;
A12: a <> b by A1, AFF_1:16;
then A13: Line a,b c= X by A4, A5, A7, Th19;
A14: Line a,b // Line a',b' by A2, A3, A12, AFF_1:51;
then consider Y being Subset of such that
A15: Line a,b c= Y and
A16: Line a',b' c= Y and
A17: Y is being_plane by Th39;
A18: b in Line a,b by AFF_1:26;
A19: a' in Line a',b' by AFF_1:26;
then A20: Line a,a' c= Y by A4, A10, A9, A15, A16, A17, Th19;
A21: b' in Line a',b' by AFF_1:26;
A22: not b' in X

proof

assume b' in X ; :: thesis: contradiction
then Line a',b' c= X by A7, A21, A14, A13, Th23;
hence contradiction by A10, A19; :: thesis: verum

end;

then A23: Line b,b' is being_line by A5, AFF_1:def 3;
A24: b' in Line b,b' by AFF_1:26;
A25: a in Line a,a' by AFF_1:26;
A26: a <> c by A1, AFF_1:16;
A27: b in Line b,b' by AFF_1:26;
A28: a' in Line a,a' by AFF_1:26;
A29: Line a,b is being_line by A12, AFF_1:def 3;
A30: Line a,a' <> Line b,b'

proof

assume Line a,a' = Line b,b' ; :: thesis: contradiction
then Line a,a' = Line a,b by A12, A9, A18, A29, A11, A25, A27, AFF_1:30;
hence contradiction by A10, A13, A28; :: thesis: verum

end;

A31: now

set C = c * (Line a,a');
assume A32: Line a,a' // Line b,b' ; :: thesis: ex c' being Element of st
( a,c // a',c' & b,c // b',c' )
A33: c in c * (Line a,a') by A11, Def3;
A34: Line a,a' <> c * (Line a,a')

proof

assume Line a,a' = c * (Line a,a') ; :: thesis: contradiction
then Line a,a' = Line a,c by A26, A11, A25, A33, AFF_1:71;
then Line a,a' c= X by A4, A6, A7, A26, Th19;
hence contradiction by A10, A28; :: thesis: verum

end;

A35: Line a,a' // c * (Line a,a') by A11, Def3;
then consider c' being Element of such that
A36: c' in c * (Line a,a') and
A37: a,c // a',c' by A25, A28, A33, Lm2;
c * (Line a,a') is being_line by A11, Th27;
then b,c // b',c' by A3, A8, A11, A23, A25, A28, A27, A24, A30, A32, A33, A35, A36, A37, A34, Th51;
hence ex c' being Element of st
( a,c // a',c' & b,c // b',c' ) by A37; :: thesis: verum

end;

A38: a' in Y by A19, A16;

A39: now

given q being Element of such that A40: q in Line a,a' and
A41: q in Line b,b' ; :: thesis: ex c' being Element of st
( a,c // a',c' & b,c // b',c' )
A42: q <> a

proof

assume q = a ; :: thesis: contradiction
then Line a,b = Line b,b' by A12, A9, A18, A29, A23, A27, A41, AFF_1:30;
hence contradiction by A13, A22, A24; :: thesis: verum

end;

A43: q <> b

proof

assume q = b ; :: thesis: contradiction
then Line a,b = Line a,a' by A12, A9, A18, A29, A11, A25, A40, AFF_1:30;
hence contradiction by A10, A13, A28; :: thesis: verum

end;

set C = Line q,c;
A44: c in Line q,c by AFF_1:26;
A45: Line a,a' <> Line q,c

proof

assume Line a,a' = Line q,c ; :: thesis: contradiction
then Line a,a' = Line a,c by A26, A11, A25, A44, AFF_1:71;
then Line a,a' c= X by A4, A6, A7, A26, Th19;
hence contradiction by A10, A28; :: thesis: verum

end;

LIN q,a,a' by A11, A25, A28, A40, AFF_1:33;
then consider c' being Element of such that
A46: LIN q,c,c' and
A47: a,c // a',c' by A42, Th1;
A48: q <> c by A1, A4, A5, A6, A7, A10, A9, A18, A15, A17, A38, A20, A40, Th25;
then A49: ( q in Line q,c & Line q,c is being_line ) by AFF_1:26, AFF_1:def 3;
then c' in Line q,c by A48, A44, A46, AFF_1:39;
then b,c // b',c' by A3, A8, A11, A23, A25, A28, A27, A24, A30, A40, A41, A42, A43, A48, A44, A49, A47, A45, Th49;
hence ex c' being Element of st
( a,c // a',c' & b,c // b',c' ) by A47; :: thesis: verum

end;

Line b,b' c= Y by A5, A18, A21, A22, A15, A16, A17, Th19;
hence ex c' being Element of st
( a,c // a',c' & b,c // b',c' ) by A17, A11, A23, A20, A31, A39, Th22; :: thesis: verum

end;

hence ex c' being Element of st
( a,c // a',c' & b,c // b',c' ) by A1, A3, A4, A5, A6, A7, Lm12; :: thesis: verum

end;

hence ex c' being Element of st
( a,c // a',c' & b,c // b',c' ) by A1, Th53; :: thesis: verum