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