let AS be AffinSpace; 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; ( 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
; X is being_plane
consider a, b, c being Element of AS such that
A3:
not LIN a,b,c
by AFF_1:21;
set P = Line a,b;
set K = Line a,c;
A4:
b in Line a,b
by AFF_1:26;
A5:
c in Line a,c
by AFF_1:26;
a <> b
by A3, AFF_1:16;
then A6:
Line a,b is being_line
by AFF_1:def 3;
set Y = Plane (Line a,c),(Line a,b);
A7:
a in Line a,b
by AFF_1:26;
a <> c
by A3, AFF_1:16;
then A8:
Line a,c is being_line
by AFF_1:def 3;
A9:
a in Line a,c
by AFF_1:26;
A10:
not Line a,c // Line a,b
proof
assume
Line a,
c // Line a,
b
;
contradiction
then
c in Line a,
b
by A7, A9, A5, AFF_1:59;
hence
contradiction
by A3, A7, A4, A6, AFF_1:33;
verum
end;
now let x be
set ;
( x in X implies x in Plane (Line a,c),(Line a,b) )assume
x in X
;
x in Plane (Line a,c),(Line a,b)then reconsider a =
x as
Element of
AS ;
set K9 =
a * (Line a,c);
A11:
a * (Line a,c) is
being_line
by A8, AFF_4:27;
A12:
Line a,
c // a * (Line a,c)
by A8, AFF_4:def 3;
then
not
a * (Line a,c) // Line a,
b
by A10, AFF_1:58;
then consider b being
Element of
AS such that A13:
b in a * (Line a,c)
and A14:
b in Line a,
b
by A1, A6, A11, AFF_1:72;
a in a * (Line a,c)
by A8, AFF_4:def 3;
then
a,
b // Line a,
c
by A12, A13, 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 A14;
hence
x in Plane (Line a,c),
(Line a,b)
by AFF_4:def 1;
verum end;
then A15:
X c= Plane (Line a,c),(Line a,b)
by TARSKI:def 3;
Plane (Line a,c),(Line a,b) is being_plane
by A6, A8, A10, AFF_4:def 2;
hence
X is being_plane
by A2, A15, XBOOLE_0:def 10; verum