let AS be AffinSpace; for M, X being Subset of AS st M is being_line & X is being_plane holds
( M '||' X iff ex N being Subset of AS st
( N c= X & ( M // N or N // M ) ) )
let M, X be Subset of AS; ( M is being_line & X is being_plane implies ( M '||' X iff ex N being Subset of AS st
( N c= X & ( M // N or N // M ) ) ) )
assume that
A1:
M is being_line
and
A2:
X is being_plane
; ( M '||' X iff ex N being Subset of AS st
( N c= X & ( M // N or N // M ) ) )
A3:
now ( ex N being Subset of AS st
( N c= X & ( M // N or N // M ) ) implies M '||' X )given N being
Subset of
AS such that A4:
N c= X
and A5:
(
M // N or
N // M )
;
M '||' Xnow for a being Element of AS
for A being Subset of AS st a in X & A is being_line & A c= M holds
a * A c= Xlet a be
Element of
AS;
for A being Subset of AS st a in X & A is being_line & A c= M holds
a * A c= Xlet A be
Subset of
AS;
( a in X & A is being_line & A c= M implies a * A c= X )assume that A6:
a in X
and A7:
A is
being_line
and A8:
A c= M
;
a * A c= X
A = M
by A1, A7, A8, Th33;
then
M // a * A
by A7, Def3;
then A9:
N // a * A
by A5, AFF_1:44;
a in a * A
by A7, Def3;
hence
a * A c= X
by A2, A4, A6, A9, Th23;
verum end; hence
M '||' X
;
verum end;
hence
( M '||' X iff ex N being Subset of AS st
( N c= X & ( M // N or N // M ) ) )
by A3; verum