let AS be AffinSpace; :: thesis: for X being Subset of st X is being_plane holds
X '||' X
let X be Subset of ; :: thesis: ( X is being_plane implies X '||' X )
assume X is being_plane ; :: thesis: X '||' X
then for a being Element of
for A being Subset of 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