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

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