let AS be AffinSpace; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( M '||' X iff ex N being Subset of AS st
( N c= X & ( M // N or N // M ) ) )
A3: now :: thesis: ( 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 ) ; :: thesis: M '||' X
now :: thesis: 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= X
let a be Element of AS; :: thesis: for A being Subset of AS st a in X & A is being_line & A c= M holds
a * A c= X
let A be Subset of AS; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum
end;
hence M '||' X ; :: thesis: verum
end;
now :: thesis: ( M '||' X implies ex N being Subset of AS st
( N c= X & ( M // N or N // M ) ) )
consider a, b, c being Element of AS such that
A10: a in X and
b in X and
c in X and
not LIN a,b,c by A2, Th34;
assume A11: M '||' X ; :: thesis: ex N being Subset of AS st
( N c= X & ( M // N or N // M ) )
take N = a * M; :: thesis: ( N c= X & ( M // N or N // M ) )
thus N c= X by A1, A11, A10; :: thesis: ( M // N or N // M )
thus ( M // N or N // M ) by A1, Def3; :: thesis: verum
end;
hence ( M '||' X iff ex N being Subset of AS st
( N c= X & ( M // N or N // M ) ) ) by A3; :: thesis: verum