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

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