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 ) ) )

( N c= X & ( M // N or N // M ) ) ) by A3; :: thesis: verum

( 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 )

( 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

end;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

hence
M '||' X
; :: thesis: verumfor 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;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

now :: thesis: ( M '||' X implies ex N being Subset of AS st

( N c= X & ( M // N or N // M ) ) )

hence
( M '||' X iff 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;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

( N c= X & ( M // N or N // M ) ) ) by A3; :: thesis: verum