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:12;
set P = Line (a,b);
set K = Line (a,c);
A4:
b in Line (a,b)
by AFF_1:15;
A5:
c in Line (a,c)
by AFF_1:15;
a <> b
by A3, AFF_1:7;
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:15;
a <> c
by A3, AFF_1:7;
then A8:
Line (a,c) is being_line
by AFF_1:def 3;
A9:
a in Line (a,c)
by AFF_1:15;
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:45;
hence
contradiction
by A3, A7, A4, A6, AFF_1:21;
verum
end;
now for x being object st x in X holds
x in Plane ((Line (a,c)),(Line (a,b)))let x be
object ;
( 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:44;
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:58;
a in a * (Line (a,c))
by A8, AFF_4:def 3;
then
a,
b // Line (
a,
c)
by A12, A13, AFF_1:40;
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)))
;
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