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,P)then 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:49;
a,
b // M
by A5, A10, AFF_1:43;
then A11:
a in M
by A9, Th2;
b,
c // M
by A7, A10, AFF_1:43;
then
c in M
by A9, Th2;
then
a,
c // K
by A10, A11, AFF_1:40;
hence
x in Plane (
K,
P)
by A3, A8;
verum end;
hence
Plane (K,Q) c= Plane (K,P)
by TARSKI:def 3; verum