let AS be AffinSpace; 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; 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; ( 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
; 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; verum