let AS be AffinSpace; :: thesis: for K, P, Q being Subset of AS st K is being_line & P is being_line & Q is being_line & not K // Q & Q c= Plane (K,P) holds

Plane (K,Q) = Plane (K,P)

let K, P, Q be Subset of AS; :: thesis: ( K is being_line & P is being_line & Q is being_line & not K // Q & Q c= Plane (K,P) implies Plane (K,Q) = Plane (K,P) )

assume that

A1: K is being_line and

A2: P is being_line and

A3: Q is being_line and

A4: not K // Q and

A5: Q c= Plane (K,P) ; :: thesis: Plane (K,Q) = Plane (K,P)

A6: Plane (K,Q) c= Plane (K,P) by A1, A5, Lm6;

consider a, b being Element of AS such that

A7: a in Q and

A8: b in Q and

A9: a <> b by A3, AFF_1:19;

consider b9 being Element of AS such that

A10: b,b9 // K and

A11: b9 in P by A5, A8, Lm3;

b9,b // K by A10, AFF_1:34;

then A12: b9 in Plane (K,Q) by A8;

consider a9 being Element of AS such that

A13: a,a9 // K and

A14: a9 in P by A5, A7, Lm3;

A15: a9 <> b9

then a9 in Plane (K,Q) by A7;

then Plane (K,P) c= Plane (K,Q) by A1, A2, A3, A14, A11, A15, A12, Lm5, Lm6;

hence Plane (K,Q) = Plane (K,P) by A6, XBOOLE_0:def 10; :: thesis: verum

Plane (K,Q) = Plane (K,P)

let K, P, Q be Subset of AS; :: thesis: ( K is being_line & P is being_line & Q is being_line & not K // Q & Q c= Plane (K,P) implies Plane (K,Q) = Plane (K,P) )

assume that

A1: K is being_line and

A2: P is being_line and

A3: Q is being_line and

A4: not K // Q and

A5: Q c= Plane (K,P) ; :: thesis: Plane (K,Q) = Plane (K,P)

A6: Plane (K,Q) c= Plane (K,P) by A1, A5, Lm6;

consider a, b being Element of AS such that

A7: a in Q and

A8: b in Q and

A9: a <> b by A3, AFF_1:19;

consider b9 being Element of AS such that

A10: b,b9 // K and

A11: b9 in P by A5, A8, Lm3;

b9,b // K by A10, AFF_1:34;

then A12: b9 in Plane (K,Q) by A8;

consider a9 being Element of AS such that

A13: a,a9 // K and

A14: a9 in P by A5, A7, Lm3;

A15: a9 <> b9

proof

a9,a // K
by A13, AFF_1:34;
consider A being Subset of AS such that

A16: a9 in A and

A17: K // A by A1, AFF_1:49;

a9,a // A by A13, A17, Th3;

then A18: a in A by A16, Th2;

assume a9 = b9 ; :: thesis: contradiction

then a9,b // A by A10, A17, Th3;

then A19: b in A by A16, Th2;

A is being_line by A17, AFF_1:36;

hence contradiction by A3, A4, A7, A8, A9, A17, A19, A18, AFF_1:18; :: thesis: verum

end;A16: a9 in A and

A17: K // A by A1, AFF_1:49;

a9,a // A by A13, A17, Th3;

then A18: a in A by A16, Th2;

assume a9 = b9 ; :: thesis: contradiction

then a9,b // A by A10, A17, Th3;

then A19: b in A by A16, Th2;

A is being_line by A17, AFF_1:36;

hence contradiction by A3, A4, A7, A8, A9, A17, A19, A18, AFF_1:18; :: thesis: verum

then a9 in Plane (K,Q) by A7;

then Plane (K,P) c= Plane (K,Q) by A1, A2, A3, A14, A11, A15, A12, Lm5, Lm6;

hence Plane (K,Q) = Plane (K,P) by A6, XBOOLE_0:def 10; :: thesis: verum