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

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