let AS be AffinSpace; :: thesis: for M, X being Subset of AS st M is being_line & X is being_plane & M c= X holds
M '||' X
let M, X be Subset of AS; :: thesis: ( M is being_line & X is being_plane & M c= X implies M '||' X )
assume that
A1: M is being_line and
A2: ( X is being_plane & M c= X ) ; :: thesis: M '||' X
M // M by A1, AFF_1:41;
hence M '||' X by A1, A2, Th41; :: thesis: verum