let AS be AffinSpace; :: thesis: for X, Y being Subset of AS st AS is AffinPlane & X is being_plane & Y is being_plane holds
X = Y
let X, Y be Subset of AS; :: thesis: ( AS is AffinPlane & X is being_plane & Y is being_plane implies X = Y )
assume that
A1: AS is AffinPlane and
A2: X is being_plane and
A3: Y is being_plane ; :: thesis: X = Y
X = the carrier of AS by A1, A2, Th2;
hence X = Y by A1, A3, Th2; :: thesis: verum