let AS be AffinSpace; :: thesis: for a being Element of AS
for K, P, Q being Subset of AS st K is being_line & P is being_line & 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 K is being_line & P is being_line & 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: ( K is being_line & P is being_line & a in Q & a in Plane K,P & K // Q implies Q c= Plane K,P )
assume A1: ( K is being_line & P is being_line & a in Q & a in Plane K,P & K // Q ) ; :: thesis: Q c= Plane K,P

now

let x be set ; :: thesis: ( x in Q implies x in Plane K,P )
assume A2: x in Q ; :: thesis: x in Plane K,P
consider b being Element of AS such that
A3: ( a,b // K & b in P ) by A1, Lm3;
A4: Plane K,P = Plane Q,P by A1, Th16;
A5: Q is being_line by A1, AFF_1:50;
a,b // Q by A1, A3, AFF_1:57;
then A6: b in Q by A1, A5, AFF_1:37;
reconsider c = x as Element of AS by A2;
c,b // Q by A2, A5, A6, AFF_1:37;
hence x in Plane K,P by A3, A4; :: thesis: verum

end;

hence Q c= Plane K,P by TARSKI:def 3; :: thesis: verum