let AS be AffinSpace; :: thesis: for a, b, c being Element of AS ex X being Subset of AS st
( a in X & b in X & c in X & X is being_plane )
let a, b, c be Element of AS; :: thesis: ex X being Subset of AS st
( a in X & b in X & c in X & X is being_plane )
consider A being Subset of AS such that
A1: ( a in A & b in A ) and
A2: A is being_line by Th11;
ex X being Subset of AS st
( c in X & A c= X & X is being_plane ) by A2, Th36;
hence ex X being Subset of AS st
( a in X & b in X & c in X & X is being_plane ) by A1; :: thesis: verum