let AS be AffinSpace; :: thesis: for q being Element of AS

for M, N being Subset of AS st q in M & q in N & M is being_line & N is being_line holds

ex X being Subset of AS st

( M c= X & N c= X & X is being_plane )

let q be Element of AS; :: thesis: for M, N being Subset of AS st q in M & q in N & M is being_line & N is being_line holds

ex X being Subset of AS st

( M c= X & N c= X & X is being_plane )

let M, N be Subset of AS; :: thesis: ( q in M & q in N & M is being_line & N is being_line implies ex X being Subset of AS st

( M c= X & N c= X & X is being_plane ) )

assume that

A1: q in M and

A2: q in N and

A3: M is being_line and

A4: N is being_line ; :: thesis: ex X being Subset of AS st

( M c= X & N c= X & X is being_plane )

consider a being Element of AS such that

A5: a <> q and

A6: a in N by A4, AFF_1:20;

A7: ex X being Subset of AS st

( a in X & M c= X & X is being_plane ) by A3, Th36;

N = Line (q,a) by A2, A4, A5, A6, AFF_1:24;

hence ex X being Subset of AS st

( M c= X & N c= X & X is being_plane ) by A1, A5, A7, Th19; :: thesis: verum

for M, N being Subset of AS st q in M & q in N & M is being_line & N is being_line holds

ex X being Subset of AS st

( M c= X & N c= X & X is being_plane )

let q be Element of AS; :: thesis: for M, N being Subset of AS st q in M & q in N & M is being_line & N is being_line holds

ex X being Subset of AS st

( M c= X & N c= X & X is being_plane )

let M, N be Subset of AS; :: thesis: ( q in M & q in N & M is being_line & N is being_line implies ex X being Subset of AS st

( M c= X & N c= X & X is being_plane ) )

assume that

A1: q in M and

A2: q in N and

A3: M is being_line and

A4: N is being_line ; :: thesis: ex X being Subset of AS st

( M c= X & N c= X & X is being_plane )

consider a being Element of AS such that

A5: a <> q and

A6: a in N by A4, AFF_1:20;

A7: ex X being Subset of AS st

( a in X & M c= X & X is being_plane ) by A3, Th36;

N = Line (q,a) by A2, A4, A5, A6, AFF_1:24;

hence ex X being Subset of AS st

( M c= X & N c= X & X is being_plane ) by A1, A5, A7, Th19; :: thesis: verum