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 that
A1: A // M and
A2: M '||' X ; :: thesis: A '||' X
A3: M is being_line by A1, AFF_1:36;
A4: A is being_line by A1, AFF_1:36;

now :: thesis: for a being Element of AS
for C being Subset of AS st a in X & C is being_line & C c= A holds
a * C c= X

consider q, p being Element of AS such that
A5: q in A and
p in A and
q <> p by A4, AFF_1:19;
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 that
A6: a in X and
A7: ( C is being_line & C c= A ) ; :: thesis: a * C c= X
A8: a * A = a * (q * M) by A1, A3, A5, Def3
.= a * M by A3, Th31 ;
C = A by A4, A7, Th33;
hence a * C c= X by A2, A3, A6, A8; :: thesis: verum

end;

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