let AS be AffinSpace; :: thesis: for K, P being Subset of AS st not K is being_line holds
Plane K,P = {}
let K, P be Subset of AS; :: thesis: ( not K is being_line implies Plane K,P = {} )
assume A1: not K is being_line ; :: thesis: Plane K,P = {}
consider x being Element of Plane K,P;
assume Plane K,P <> {} ; :: thesis: contradiction
then x in Plane K,P ;
then ex a being Element of AS st
( x = a & ex b being Element of AS st
( a,b // K & b in P ) ) ;
hence contradiction by A1, AFF_1:40; :: thesis: verum