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

( 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