let AS be AffinSpace; :: thesis: for a, b, c, a9, b9, c9 being Element of AS

for A, C, P being Subset of AS st AS is not AffinPlane & A // P & A // C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 holds

b,c // b9,c9

let a, b, c, a9, b9, c9 be Element of AS; :: thesis: for A, C, P being Subset of AS st AS is not AffinPlane & A // P & A // C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 holds

b,c // b9,c9

let A, C, P be Subset of AS; :: thesis: ( AS is not AffinPlane & A // P & A // C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 implies b,c // b9,c9 )

assume that

A1: AS is not AffinPlane and

A2: A // P and

A3: A // C and

A4: ( a in A & a9 in A ) and

A5: ( b in P & b9 in P ) and

A6: ( c in C & c9 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 // a9,b9 and

A13: a,c // a9,c9 ; :: thesis: b,c // b9,c9

for A, C, P being Subset of AS st AS is not AffinPlane & A // P & A // C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 holds

b,c // b9,c9

let a, b, c, a9, b9, c9 be Element of AS; :: thesis: for A, C, P being Subset of AS st AS is not AffinPlane & A // P & A // C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 holds

b,c // b9,c9

let A, C, P be Subset of AS; :: thesis: ( AS is not AffinPlane & A // P & A // C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 implies b,c // b9,c9 )

assume that

A1: AS is not AffinPlane and

A2: A // P and

A3: A // C and

A4: ( a in A & a9 in A ) and

A5: ( b in P & b9 in P ) and

A6: ( c in C & c9 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 // a9,b9 and

A13: a,c // a9,c9 ; :: thesis: b,c // b9,c9

now :: thesis: ( A,P,C is_coplanar implies b,c // b9,c9 )

hence
b,c // b9,c9
by A2, A3, A4, A5, A6, A7, A10, A11, A12, A13, Lm11; :: thesis: verumassume
A,P,C is_coplanar
; :: thesis: b,c // b9,c9

then consider X being Subset of AS such that

A14: A c= X and

A15: P c= X and

A16: C c= X and

A17: X is being_plane ;

consider d being Element of AS 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 d9 being Element of AS st

( d9 in d * A & a,d // a9,d9 )

A27: d9 in d * A and

A28: a,d // a9,d9 ;

A29: ( d * A // P & d * A // C ) by A2, A3, A21, AFF_1:44;

end;then consider X being Subset of AS such that

A14: A c= X and

A15: P c= X and

A16: C c= X and

A17: X is being_plane ;

consider d being Element of AS 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 d9 being Element of AS st

( d9 in d * A & a,d // a9,d9 )

proof

( d9 in d * A & a,d // a9,d9 ) by A22; :: thesis: verum

end;

then consider d9 being Element of AS such that A22: now :: thesis: ( a <> a9 implies ex d9 being Element of AS st

( d9 in d * A & a,d // a9,d9 ) )

( d9 in d * A & a,d // a9,d9 ) )

assume A23:
a <> a9
; :: thesis: ex d9 being Element of AS st

( d9 in d * A & a,d // a9,d9 )

consider d9 being Element of AS such that

A24: a,a9 // d,d9 and

A25: a,d // a9,d9 by DIRAF:40;

d,d9 // a,a9 by A24, AFF_1:4;

then d,d9 // A by A4, A7, A23, AFF_1:27;

then d,d9 // d * A by A21, Th3;

then d9 in d * A by A19, Th2;

hence ex d9 being Element of AS st

( d9 in d * A & a,d // a9,d9 ) by A25; :: thesis: verum

end;( d9 in d * A & a,d // a9,d9 )

consider d9 being Element of AS such that

A24: a,a9 // d,d9 and

A25: a,d // a9,d9 by DIRAF:40;

d,d9 // a,a9 by A24, AFF_1:4;

then d,d9 // A by A4, A7, A23, AFF_1:27;

then d,d9 // d * A by A21, Th3;

then d9 in d * A by A19, Th2;

hence ex d9 being Element of AS st

( d9 in d * A & a,d // a9,d9 ) by A25; :: thesis: verum

now :: thesis: ( a = a9 implies ex d9 being Element of AS st

( d9 in d * A & a,d // a9,d9 ) )

hence
ex d9 being Element of AS st ( d9 in d * A & a,d // a9,d9 ) )

assume A26:
a = a9
; :: thesis: ex d9 being Element of AS st

( d9 in d * A & a,d // a9,d9 )

take d9 = d; :: thesis: ( d9 in d * A & a,d // a9,d9 )

thus d9 in d * A by A7, Def3; :: thesis: a,d // a9,d9

thus a,d // a9,d9 by A26, AFF_1:2; :: thesis: verum

end;( d9 in d * A & a,d // a9,d9 )

take d9 = d; :: thesis: ( d9 in d * A & a,d // a9,d9 )

thus d9 in d * A by A7, Def3; :: thesis: a,d // a9,d9

thus a,d // a9,d9 by A26, AFF_1:2; :: thesis: verum

( d9 in d * A & a,d // a9,d9 ) by A22; :: thesis: verum

A27: d9 in d * A and

A28: a,d // a9,d9 ;

A29: ( d * A // P & d * A // C ) by A2, A3, A21, AFF_1:44;

now :: thesis: ( P <> C implies b,c // b9,c9 )

hence
b,c // b9,c9
by A5, A6, A8, AFF_1:51; :: thesis: verumassume A30:
P <> C
; :: thesis: b,c // b9,c9

A31: not d * A,P,C is_coplanar

not A,d * A,P is_coplanar

A34: ( d * A <> P & d * A <> C ) by A15, A16, A18, A19;

not A,d * A,C is_coplanar

hence b,c // b9,c9 by A5, A6, A7, A19, A29, A27, A34, A31, A33, Lm11, Th27; :: thesis: verum

end;A31: not d * A,P,C is_coplanar

proof

A32:
d * A <> A
by A14, A18, A19;
assume
d * A,P,C is_coplanar
; :: thesis: contradiction

then P,C,d * A is_coplanar ;

hence contradiction by A8, A9, A15, A16, A17, A20, A30, Th46; :: thesis: verum

end;then P,C,d * A is_coplanar ;

hence contradiction by A8, A9, A15, A16, A17, A20, A30, Th46; :: thesis: verum

not A,d * A,P is_coplanar

proof

then A33:
d,b // d9,b9
by A2, A4, A5, A7, A10, A12, A19, A21, A27, A28, A32, Lm11;
assume
A,d * A,P is_coplanar
; :: thesis: contradiction

then A,P,d * A is_coplanar ;

hence contradiction by A7, A8, A10, A14, A15, A17, A20, Th46; :: thesis: verum

end;then A,P,d * A is_coplanar ;

hence contradiction by A7, A8, A10, A14, A15, A17, A20, Th46; :: thesis: verum

A34: ( d * A <> P & d * A <> C ) by A15, A16, A18, A19;

not A,d * A,C is_coplanar

proof

then
d,c // d9,c9
by A3, A4, A6, A7, A11, A13, A19, A21, A27, A28, A32, Lm11;
assume
A,d * A,C is_coplanar
; :: thesis: contradiction

then A,C,d * A is_coplanar ;

hence contradiction by A7, A9, A11, A14, A16, A17, A20, Th46; :: thesis: verum

end;then A,C,d * A is_coplanar ;

hence contradiction by A7, A9, A11, A14, A16, A17, A20, Th46; :: thesis: verum

hence b,c // b9,c9 by A5, A6, A7, A19, A29, A27, A34, A31, A33, Lm11, Th27; :: thesis: verum