let AS be AffinSpace; for K, P being Subset of AS st not K is being_line holds
Plane (K,P) = {}
let K, P be Subset of AS; ( not K is being_line implies Plane (K,P) = {} )
assume A1:
not K is being_line
; Plane (K,P) = {}
set x = the Element of Plane (K,P);
assume
Plane (K,P) <> {}
; 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; verum