let AS be AffinSpace; :: thesis: for K, P, Q being Subset of AS st K is being_line & Q c= Plane (K,P) holds
Plane (K,Q) c= Plane (K,P)
let K, P, Q be Subset of AS; :: thesis: ( 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) ; :: thesis: Plane (K,Q) c= Plane (K,P)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Plane (K,Q) or x in Plane (K,P) )
assume x in Plane (K,Q) ; :: thesis: 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; :: thesis: verum