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 in A & a in X & A '||' X holds
A c= X
let a be Element of AS; for A, X being Subset of AS st A is being_line & X is being_plane & a in A & a in X & A '||' X holds
A c= X
let A, X be Subset of AS; ( A is being_line & X is being_plane & a in A & a in X & A '||' X implies A c= X )
assume that
A1:
A is being_line
and
A2:
X is being_plane
and
A3:
a in A
and
A4:
a in X
and
A5:
A '||' X
; A c= X
consider N being Subset of AS such that
A6:
N c= X
and
A7:
( A // N or N // A )
by A1, A2, A5, Th41;
A8:
N is being_line
by A7, AFF_1:36;
A =
a * A
by A1, A3, Lm8
.=
a * N
by A7, Th32
;
hence
A c= X
by A2, A4, A6, A8, Th28; verum