let AS be AffinSpace; :: thesis: for a, b, c, a9, b9 being Element of AS st AS is AffinPlane & not LIN a,b,c holds
ex c9 being Element of AS st
( a,c // a9,c9 & b,c // b9,c9 )
let a, b, c, a9, b9 be Element of AS; :: thesis: ( AS is AffinPlane & not LIN a,b,c implies ex c9 being Element of AS st
( a,c // a9,c9 & b,c // b9,c9 ) )
assume that
A1: AS is AffinPlane and
A2: not LIN a,b,c ; :: thesis: ex c9 being Element of AS st
( a,c // a9,c9 & b,c // b9,c9 )
consider C being Subset of AS such that
A3: ( b in C & c in C ) and
A4: C is being_line by Th11;
consider N being Subset of AS such that
A5: b9 in N and
A6: C // N by A4, AFF_1:49;
A7: N is being_line by A6, AFF_1:36;
consider P being Subset of AS such that
A8: a in P and
A9: c in P and
A10: P is being_line by Th11;
consider M being Subset of AS such that
A11: a9 in M and
A12: P // M by A10, AFF_1:49;
A13: not M // N
proof
assume M // N ; :: thesis: contradiction
then N // P by A12, AFF_1:44;
then C // P by A6, AFF_1:44;
then b in P by A3, A9, AFF_1:45;
hence contradiction by A2, A8, A9, A10, AFF_1:21; :: thesis: verum
end;
M is being_line by A12, AFF_1:36;
then consider c9 being Element of AS such that
A14: c9 in M and
A15: c9 in N by A1, A7, A13, AFF_1:58;
A16: b,c // b9,c9 by A3, A5, A6, A15, AFF_1:39;
a,c // a9,c9 by A8, A9, A11, A12, A14, AFF_1:39;
hence ex c9 being Element of AS st
( a,c // a9,c9 & b,c // b9,c9 ) by A16; :: thesis: verum