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

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