let AS be AffinSpace; :: thesis: for X being Subset of AS st X is being_plane holds
X '||' X
let X be Subset of AS; :: thesis: ( X is being_plane implies X '||' X )
assume X is being_plane ; :: thesis: X '||' X
then for a being Element of AS
for A being Subset of AS st a in X & A is being_line & A c= X holds
a * A c= X by Th28;
hence X '||' X by Def4; :: thesis: verum