let AS be AffinSpace; :: thesis: for X being Subset of AS st AS is AffinPlane & X = the carrier of AS holds
X is being_plane
let X be Subset of AS; :: thesis: ( AS is AffinPlane & X = the carrier of AS implies X is being_plane )
assume that
A1: AS is AffinPlane and
A2: X = the carrier of AS ; :: thesis: X is being_plane
consider a, b, c being Element of AS such that
A3: not LIN a,b,c by AFF_1:21;
A4: ( a <> b & a <> c ) by A3, AFF_1:16;
set P = Line a,b;
set K = Line a,c;
A5: ( a in Line a,b & a in Line a,c & b in Line a,b & c in Line a,c & Line a,b is being_line & Line a,c is being_line ) by A4, AFF_1:26, AFF_1:def 3;
A6: not Line a,c // Line a,b

proof

assume Line a,c // Line a,b ; :: thesis: contradiction
then c in Line a,b by A5, AFF_1:59;
hence contradiction by A3, A5, AFF_1:33; :: thesis: verum

end;

set Y = Plane (Line a,c),(Line a,b);
A7: Plane (Line a,c),(Line a,b) is being_plane by A5, A6, AFF_4:def 2;

now

let x be set ; :: thesis: ( x in X implies x in Plane (Line a,c),(Line a,b) )
assume x in X ; :: thesis: x in Plane (Line a,c),(Line a,b)
then reconsider a = x as Element of AS ;
set K' = a * (Line a,c);
A8: ( a * (Line a,c) is being_line & Line a,c // a * (Line a,c) & a in a * (Line a,c) ) by A5, AFF_4:27, AFF_4:def 3;
then not a * (Line a,c) // Line a,b by A6, AFF_1:58;
then consider b being Element of AS such that
A9: ( b in a * (Line a,c) & b in Line a,b ) by A1, A5, A8, AFF_1:72;
a,b // Line a,c by A8, A9, AFF_1:54;
then a in { zz where zz is Element of AS : ex b being Element of AS st
( zz,b // Line a,c & b in Line a,b ) } by A9;
hence x in Plane (Line a,c),(Line a,b) by AFF_4:def 1; :: thesis: verum

end;

then X c= Plane (Line a,c),(Line a,b) by TARSKI:def 3;
hence X is being_plane by A2, A7, XBOOLE_0:def 10; :: thesis: verum