let A be Subset of (TOP-REAL 3); for B being non empty convex Subset of (TOP-REAL 2)
for r being Real
for x being Element of (TOP-REAL 3) st A = { x where x is Element of (TOP-REAL 3) : ( |[(x `1),(x `2)]| in B & x `3 = r ) } holds
( not A is empty & A is convex )
let B be non empty convex Subset of (TOP-REAL 2); for r being Real
for x being Element of (TOP-REAL 3) st A = { x where x is Element of (TOP-REAL 3) : ( |[(x `1),(x `2)]| in B & x `3 = r ) } holds
( not A is empty & A is convex )
let r be Real; for x being Element of (TOP-REAL 3) st A = { x where x is Element of (TOP-REAL 3) : ( |[(x `1),(x `2)]| in B & x `3 = r ) } holds
( not A is empty & A is convex )
let x be Element of (TOP-REAL 3); ( A = { x where x is Element of (TOP-REAL 3) : ( |[(x `1),(x `2)]| in B & x `3 = r ) } implies ( not A is empty & A is convex ) )
assume A1:
A = { x where x is Element of (TOP-REAL 3) : ( |[(x `1),(x `2)]| in B & x `3 = r ) }
; ( not A is empty & A is convex )
A2:
for z being Element of (TOP-REAL 3) holds
( z in A iff ( |[(z `1),(z `2)]| in B & z `3 = r ) )
set y = the Element of B;
reconsider z = |[( the Element of B `1),( the Element of B `2),r]| as Element of (TOP-REAL 3) ;
z = |[(z `1),(z `2),(z `3)]|
by EUCLID_5:3;
then A3:
( z `1 = the Element of B `1 & z `2 = the Element of B `2 & z `3 = r )
by FINSEQ_1:78;
the Element of B in B
;
then
( |[(z `1),(z `2)]| in B & z `3 = r )
by A3, EUCLID:53;
then
z in A
by A1;
hence
not A is empty
; A is convex
now for u, v being Element of (TOP-REAL 3)
for s being Real st 0 < s & s < 1 & u in A & v in A holds
(s * u) + ((1 - s) * v) in Alet u,
v be
Element of
(TOP-REAL 3);
for s being Real st 0 < s & s < 1 & u in A & v in A holds
(s * u) + ((1 - s) * v) in Alet s be
Real;
( 0 < s & s < 1 & u in A & v in A implies (s * u) + ((1 - s) * v) in A )assume that A4:
(
0 < s &
s < 1 )
and A5:
u in A
and A6:
v in A
;
(s * u) + ((1 - s) * v) in Areconsider w =
(s * u) + ((1 - s) * v) as
Element of
(TOP-REAL 3) ;
now ( w `3 = r & |[(w `1),(w `2)]| in B )reconsider su =
s * u,
sv =
(1 - s) * v as
Element of
(TOP-REAL 3) ;
(
su = |[(s * (u `1)),(s * (u `2)),(s * (u `3))]| &
sv = |[((1 - s) * (v `1)),((1 - s) * (v `2)),((1 - s) * (v `3))]| )
by EUCLID_5:7;
then A7:
|[((s * (u `1)) + ((1 - s) * (v `1))),((s * (u `2)) + ((1 - s) * (v `2))),((s * (u `3)) + ((1 - s) * (v `3)))]| =
w
by EUCLID_5:6
.=
|[(w `1),(w `2),(w `3)]|
by EUCLID_5:3
;
then A8:
(
w `1 = (s * (u `1)) + ((1 - s) * (v `1)) &
w `2 = (s * (u `2)) + ((1 - s) * (v `2)) &
w `3 = (s * (u `3)) + ((1 - s) * (v `3)) )
by FINSEQ_1:78;
(
u `3 = r &
v `3 = r )
by A5, A6, A2;
hence
w `3 = r
by A7, FINSEQ_1:78;
|[(w `1),(w `2)]| in Breconsider u9 =
|[(u `1),(u `2)]|,
v9 =
|[(v `1),(v `2)]|,
w9 =
|[(w `1),(w `2)]| as
Element of
(TOP-REAL 2) ;
hence
|[(w `1),(w `2)]| in B
by A4, CONVEX1:def 2;
verum end; hence
(s * u) + ((1 - s) * v) in A
by A1;
verum end;
hence
A is convex
by CONVEX1:def 2; verum