let AS be AffinSpace; :: thesis: for X being Subset of AS st X = the carrier of AS & X is being_plane holds
AS is AffinPlane
let X be Subset of AS; :: thesis: ( X = the carrier of AS & X is being_plane implies AS is AffinPlane )
assume that
A1: X = the carrier of AS and
A2: X is being_plane ; :: thesis: AS is AffinPlane
assume AS is not AffinPlane ; :: thesis: contradiction
then not for zz being Element of AS holds zz in X by A2, AFF_4:48;
hence contradiction by A1; :: thesis: verum