set P = Plane (p,q);
for w1, w2 being Point of (TOP-REAL n) st w1 in Plane (p,q) & w2 in Plane (p,q) holds
LSeg (w1,w2) c= Plane (p,q)
proof
let w1,
w2 be
Point of
(TOP-REAL n);
( w1 in Plane (p,q) & w2 in Plane (p,q) implies LSeg (w1,w2) c= Plane (p,q) )
assume A1:
(
w1 in Plane (
p,
q) &
w2 in Plane (
p,
q) )
;
LSeg (w1,w2) c= Plane (p,q)
reconsider n0 =
n as
Nat ;
reconsider p0 =
p,
q0 =
q as
Point of
(TOP-REAL n0) ;
A2:
Plane (
p,
q)
= { y where y is Point of (TOP-REAL n0) : |(p0,(y - q0))| = 0 }
by MFOLD_2:def 2;
consider v1 being
Point of
(TOP-REAL n0) such that A3:
(
w1 = v1 &
|(p0,(v1 - q0))| = 0 )
by A1, A2;
consider v2 being
Point of
(TOP-REAL n0) such that A4:
(
w2 = v2 &
|(p0,(v2 - q0))| = 0 )
by A1, A2;
for
x being
object st
x in LSeg (
w1,
w2) holds
x in Plane (
p,
q)
proof
let x be
object ;
( x in LSeg (w1,w2) implies x in Plane (p,q) )
assume A5:
x in LSeg (
w1,
w2)
;
x in Plane (p,q)
then reconsider w =
x as
Point of
(TOP-REAL n0) ;
reconsider r1 = 1 as
Real ;
consider r being
Real such that A6:
(
0 <= r &
r <= 1 &
w = ((1 - r) * w1) + (r * w2) )
by A5, RLTOPSP1:76;
A7:
|(p0,((1 - r) * (v1 - q0)))| =
(1 - r) * 0
by A3, EUCLID_2:20
.=
0
;
A8:
|(p0,(r * (v2 - q0)))| =
r * 0
by A4, EUCLID_2:20
.=
0
;
A9:
((1 - r) * (v1 - q0)) + (r * (v2 - q0)) =
((1 - r) * (w1 - q)) + ((r * w2) - (r * q))
by A3, A4, RLVECT_1:34
.=
(((1 - r) * w1) - ((1 - r) * q)) + ((r * w2) - (r * q))
by RLVECT_1:34
.=
(((1 - r) * w1) + ((- (1 - r)) * q)) + ((r * w2) - (r * q))
by RLVECT_1:79
.=
(((1 - r) * w1) + ((r - 1) * q)) + ((r * w2) - (r * q))
.=
(((1 - r) * w1) + ((r * q) - (r1 * q))) + ((r * w2) - (r * q))
by RLVECT_1:35
.=
((1 - r) * w1) + (((r * q) - (r1 * q)) + ((r * w2) - (r * q)))
by RLVECT_1:def 3
.=
((1 - r) * w1) + ((((- (r1 * q)) + (r * q)) + (- (r * q))) + (r * w2))
by RLVECT_1:def 3
.=
((1 - r) * w1) + (((- (r1 * q)) + ((r * q) - (r * q))) + (r * w2))
by RLVECT_1:def 3
.=
((1 - r) * w1) + (((- (r1 * q)) + (0. (TOP-REAL n))) + (r * w2))
by RLVECT_1:5
.=
((1 - r) * w1) + ((- (r1 * q)) + (r * w2))
by RLVECT_1:4
.=
(((1 - r) * w1) + (r * w2)) + (- (r1 * q))
by RLVECT_1:def 3
.=
w + (- q0)
by A6, RLVECT_1:def 8
.=
w - q0
;
0 =
|(p0,((1 - r) * (v1 - q0)))| + |(p0,(r * (v2 - q0)))|
by A7, A8
.=
|(p0,(w - q0))|
by A9, EUCLID_2:26
;
hence
x in Plane (
p,
q)
by A2;
verum
end;
hence
LSeg (
w1,
w2)
c= Plane (
p,
q)
;
verum
end;
then
Plane (p,q) is convex Subset of (TOP-REAL n)
by RLTOPSP1:22;
then
[#] ((TOP-REAL n) | (Plane (p,q))) is convex Subset of (TOP-REAL n)
by PRE_TOPC:def 5;
then
[#] (TPlane (p,q)) is convex Subset of (TOP-REAL n)
by MFOLD_2:def 3;
hence
TPlane (p,q) is convex
by TOPALG_2:def 1; verum