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