let AS be AffinSpace; for a being Element of AS
for A, X being Subset of AS st A is being_line & X is being_plane & A '||' X holds
a * A c= a + X
let a be Element of AS; for A, X being Subset of AS st A is being_line & X is being_plane & A '||' X holds
a * A c= a + X
let A, X be Subset of AS; ( A is being_line & X is being_plane & A '||' X implies a * A c= a + X )
assume that
A1:
A is being_line
and
A2:
X is being_plane
and
A3:
A '||' X
; a * A c= a + X
A4:
( X '||' a + X & a in a + X )
by A2, Def6;
consider N being Subset of AS such that
A5:
N c= X
and
A6:
( A // N or N // A )
by A1, A2, A3, Th41;
( a * A = a * N & N is being_line )
by A6, Th32, AFF_1:36;
hence
a * A c= a + X
by A5, A4; verum