let AS be AffinSpace; :: thesis: for a being Element of AS

for K, P, Q being Subset of AS st a in Q & a in Plane (K,P) & K // Q holds

Q c= Plane (K,P)

let a be Element of AS; :: thesis: for K, P, Q being Subset of AS st a in Q & a in Plane (K,P) & K // Q holds

Q c= Plane (K,P)

let K, P, Q be Subset of AS; :: thesis: ( a in Q & a in Plane (K,P) & K // Q implies Q c= Plane (K,P) )

assume that

A1: a in Q and

A2: a in Plane (K,P) and

A3: K // Q ; :: thesis: Q c= Plane (K,P)

A4: Plane (K,P) = Plane (Q,P) by A3, Th16;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Q or x in Plane (K,P) )

assume A5: x in Q ; :: thesis: x in Plane (K,P)

reconsider c = x as Element of AS by A5;

A6: Q is being_line by A3, AFF_1:36;

consider b being Element of AS such that

A7: a,b // K and

A8: b in P by A2, Lm3;

a,b // Q by A3, A7, AFF_1:43;

then b in Q by A1, A6, AFF_1:23;

then c,b // Q by A5, A6, AFF_1:23;

hence x in Plane (K,P) by A8, A4; :: thesis: verum

for K, P, Q being Subset of AS st a in Q & a in Plane (K,P) & K // Q holds

Q c= Plane (K,P)

let a be Element of AS; :: thesis: for K, P, Q being Subset of AS st a in Q & a in Plane (K,P) & K // Q holds

Q c= Plane (K,P)

let K, P, Q be Subset of AS; :: thesis: ( a in Q & a in Plane (K,P) & K // Q implies Q c= Plane (K,P) )

assume that

A1: a in Q and

A2: a in Plane (K,P) and

A3: K // Q ; :: thesis: Q c= Plane (K,P)

A4: Plane (K,P) = Plane (Q,P) by A3, Th16;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Q or x in Plane (K,P) )

assume A5: x in Q ; :: thesis: x in Plane (K,P)

reconsider c = x as Element of AS by A5;

A6: Q is being_line by A3, AFF_1:36;

consider b being Element of AS such that

A7: a,b // K and

A8: b in P by A2, Lm3;

a,b // Q by A3, A7, AFF_1:43;

then b in Q by A1, A6, AFF_1:23;

then c,b // Q by A5, A6, AFF_1:23;

hence x in Plane (K,P) by A8, A4; :: thesis: verum