let AS be AffinSpace; for K, Q, P being Subset of AS st K is being_line & Q c= Plane K,P holds
Plane K,Q c= Plane K,P
let K, Q, P be Subset of AS; ( K is being_line & Q c= Plane K,P implies Plane K,Q c= Plane K,P )
assume that
A1:
K is being_line
and
A2:
Q c= Plane K,P
; Plane K,Q c= Plane K,P
now let x be
set ;
( x in Plane K,Q implies x in Plane K,P )assume
x in Plane K,
Q
;
x in Plane K,Pthen consider a being
Element of
AS such that A3:
x = a
and A4:
ex
b being
Element of
AS st
(
a,
b // K &
b in Q )
;
consider b being
Element of
AS such that A5:
a,
b // K
and A6:
b in Q
by A4;
consider c being
Element of
AS such that A7:
b,
c // K
and A8:
c in P
by A2, A6, Lm3;
consider M being
Subset of
AS such that A9:
b in M
and A10:
K // M
by A1, AFF_1:63;
a,
b // M
by A5, A10, AFF_1:57;
then A11:
a in M
by A9, Th2;
b,
c // M
by A7, A10, AFF_1:57;
then
c in M
by A9, Th2;
then
a,
c // K
by A10, A11, AFF_1:54;
hence
x in Plane K,
P
by A3, A8;
verum end;
hence
Plane K,Q c= Plane K,P
by TARSKI:def 3; verum