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