let AS be AffinSpace; :: thesis: for M, N being Subset of AS st M // N holds

ex X being Subset of AS st

( M c= X & N c= X & X is being_plane )

let M, N be Subset of AS; :: thesis: ( M // N implies ex X being Subset of AS st

( M c= X & N c= X & X is being_plane ) )

assume A1: M // N ; :: thesis: ex X being Subset of AS st

( M c= X & N c= X & X is being_plane )

then N is being_line by AFF_1:36;

then consider a, b being Element of AS such that

A2: a in N and

b in N and

a <> b by AFF_1:19;

A3: M is being_line by A1, AFF_1:36;

then A4: ex X being Subset of AS st

( a in X & M c= X & X is being_plane ) by Th36;

N = a * M by A1, A3, A2, Def3;

hence ex X being Subset of AS st

( M c= X & N c= X & X is being_plane ) by A3, A4, Th28; :: thesis: verum

ex X being Subset of AS st

( M c= X & N c= X & X is being_plane )

let M, N be Subset of AS; :: thesis: ( M // N implies ex X being Subset of AS st

( M c= X & N c= X & X is being_plane ) )

assume A1: M // N ; :: thesis: ex X being Subset of AS st

( M c= X & N c= X & X is being_plane )

then N is being_line by AFF_1:36;

then consider a, b being Element of AS such that

A2: a in N and

b in N and

a <> b by AFF_1:19;

A3: M is being_line by A1, AFF_1:36;

then A4: ex X being Subset of AS st

( a in X & M c= X & X is being_plane ) by Th36;

N = a * M by A1, A3, A2, Def3;

hence ex X being Subset of AS st

( M c= X & N c= X & X is being_plane ) by A3, A4, Th28; :: thesis: verum