let AS be AffinSpace; :: thesis: for A, M, X being Subset of AS st A // M & M '||' X holds
A '||' X
let A, M, X be Subset of AS; :: thesis: ( A // M & M '||' X implies A '||' X )
assume A1: ( A // M & M '||' X ) ; :: thesis: A '||' X
then A2: ( A is being_line & M is being_line ) by AFF_1:50;

now

let a be Element of AS; :: thesis: for C being Subset of AS st a in X & C is being_line & C c= A holds
a * C c= X
let C be Subset of AS; :: thesis: ( a in X & C is being_line & C c= A implies a * C c= X )
assume A3: ( a in X & C is being_line & C c= A ) ; :: thesis: a * C c= X
then A4: C = A by A2, Th33;
consider q, p being Element of AS such that
A5: ( q in A & p in A & q <> p ) by A2, AFF_1:31;
a * A = a * (q * M) by A1, A2, A5, Def3
.= a * M by A2, Th31 ;
hence a * C c= X by A1, A2, A3, A4, Def4; :: thesis: verum

end;

hence A '||' X by Def4; :: thesis: verum