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

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