let AS be AffinSpace; :: thesis: for X being Subset of AS st AS is AffinPlane & X is being_plane holds
X = the carrier of AS
let X be Subset of AS; :: thesis: ( AS is AffinPlane & X is being_plane implies X = the carrier of AS )
assume that
A1: AS is AffinPlane and
A2: X is being_plane ; :: thesis: X = the carrier of AS
the carrier of AS c= the carrier of AS ;
then reconsider Z = the carrier of AS as Subset of AS ;
Z is being_plane by A1, Th1;
hence X = the carrier of AS by A2, AFF_4:33; :: thesis: verum