let AS be AffinSpace; :: thesis: for X being Subset of AS st X is being_plane holds
X <> {}
let X be Subset of AS; :: thesis: ( X is being_plane implies X <> {} )
assume X is being_plane ; :: thesis: X <> {}
then ex a, b, c being Element of AS st
( a in X & b in X & c in X & not LIN a,b,c ) by Th34;
hence X <> {} ; :: thesis: verum