let AS be AffinSpace; 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; ( 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)
; 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
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
;
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;
verum
end;
a9,a // K
by A13, AFF_1:34;
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; verum