let AS be AffinSpace; :: thesis: for a being Element of AS
for M, X being Subset of AS st X is being_plane & M is being_line & a in X & M c= X holds
a * M c= X
let a be Element of AS; :: thesis: for M, X being Subset of AS st X is being_plane & M is being_line & a in X & M c= X holds
a * M c= X
let M, X be Subset of AS; :: thesis: ( X is being_plane & M is being_line & a in X & M c= X implies a * M c= X )
assume that
A1: X is being_plane and
A2: M is being_line and
A3: ( a in X & M c= X ) ; :: thesis: a * M c= X
set N = a * M;
( a in a * M & M // a * M ) by A2, Def3;
hence a * M c= X by A1, A3, Th23; :: thesis: verum