let A be Subset of (TOP-REAL 3); :: thesis: 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); :: thesis: 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; :: thesis: 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); :: thesis: ( 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 ) } ; :: thesis: ( 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 ) )

proof

let z be Element of (TOP-REAL 3); :: thesis: ( z in A iff ( |[(z `1),(z `2)]| in B & z `3 = r ) )

hereby :: thesis: ( |[(z `1),(z `2)]| in B & z `3 = r implies z in A )

assume z in A ; :: thesis: ( |[(z `1),(z `2)]| in B & z `3 = r )
then ex z9 being Element of (TOP-REAL 3) st
( z = z9 & |[(z9 `1),(z9 `2)]| in B & z9 `3 = r ) by A1;
hence ( |[(z `1),(z `2)]| in B & z `3 = r ) ; :: thesis: verum

end;

assume ( |[(z `1),(z `2)]| in B & z `3 = r ) ; :: thesis: z in A
hence z in A by A1; :: thesis: verum

end;

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 ; :: thesis: A is convex

now :: thesis: 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 A

let u, v be Element of (TOP-REAL 3); :: thesis: for s being Real st 0 < s & s < 1 & u in A & v in A holds
(s * u) + ((1 - s) * v) in A
let s be Real; :: thesis: ( 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 ; :: thesis: (s * u) + ((1 - s) * v) in A
reconsider w = (s * u) + ((1 - s) * v) as Element of (TOP-REAL 3) ;

now :: thesis: ( 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; :: thesis: |[(w `1),(w `2)]| in B
reconsider u9 = |[(u `1),(u `2)]|, v9 = |[(v `1),(v `2)]|, w9 = |[(w `1),(w `2)]| as Element of (TOP-REAL 2) ;

now :: thesis: ( u9 in B & v9 in B & |[(w `1),(w `2)]| = (s * u9) + ((1 - s) * v9) )

thus ( u9 in B & v9 in B ) by A2, A6, A5; :: thesis: |[(w `1),(w `2)]| = (s * u9) + ((1 - s) * v9)
thus |[(w `1),(w `2)]| = |[(s * (u `1)),(s * (u `2))]| + |[((1 - s) * (v `1)),((1 - s) * (v `2))]| by A8, EUCLID:56
.= (s * |[(u `1),(u `2)]|) + |[((1 - s) * (v `1)),((1 - s) * (v `2))]| by EUCLID:58
.= (s * u9) + ((1 - s) * v9) by EUCLID:58 ; :: thesis: verum

end;

hence |[(w `1),(w `2)]| in B by A4, CONVEX1:def 2; :: thesis: verum

end;

hence (s * u) + ((1 - s) * v) in A by A1; :: thesis: verum

end;

hence A is convex by CONVEX1:def 2; :: thesis: verum