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) = {}
set x = the Element of Plane (K,P);
assume Plane (K,P) <> {} ; :: thesis: contradiction
then the Element of Plane (K,P) in Plane (K,P) ;
then ex a being Element of AS st
( the Element of Plane (K,P) = a & ex b being Element of AS st
( a,b // K & b in P ) ) ;
hence contradiction by A1, AFF_1:26; :: thesis: verum