let AS be AffinSpace; :: thesis: for K, P being Subset of AS st K is being_line holds
P c= Plane K,P
let K, P be Subset of AS; :: thesis: ( K is being_line implies P c= Plane K,P )
assume A1: K is being_line ; :: thesis: P c= Plane K,P

now

let x be set ; :: thesis: ( x in P implies x in Plane K,P )
assume A2: x in P ; :: thesis: x in Plane K,P
then reconsider a = x as Element of AS ;
( a,a // K & a in P ) by A1, A2, AFF_1:47;
hence x in Plane K,P ; :: thesis: verum

end;

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