proof

let c₂, c₃ be Subset of REAL ;
assume E7: for b₁, b₂ being real number holds
( ( b₁ in c₂ & b₂ in c₃ ) implies ( b₁ <= b₂ ) ) ;

per cases not ( not c₂ = 0 & not c₃ = 0 & not ( c₂ <> 0 & c₃ <> 0 ) ) ;

suppose E8: ( c₂ = 0 or c₃ = 0 ) ;

take 1 ;
thus for b₁, b₂ being real number holds
( ( b₁ in c₂ & b₂ in c₃ ) implies ( ( b₁ <= 1 & 1 <= b₂ ) ) ) by E8;

end;

suppose that E8: c₂ <> 0 and
E9: c₃ <> 0 ;

consider c₄ being Element of REAL such that
E10: c₄ in c₂ by E8, SUBSET_1:10;
consider c₅ being Element of REAL such that
E11: c₅ in c₃ by E9, SUBSET_1:10;
E12: REAL c= REAL+ \/ [:{0},REAL+ :] by NUMBERS:def 1, XBOOLE_1:36;
then E13: c₂ c= REAL+ \/ [:{0},REAL+ :] by XBOOLE_1:1;
E14: c₃ c= REAL+ \/ [:{0},REAL+ :] by E12, XBOOLE_1:1;
thus ex b₁ being real number st
for b₂, b₃ being real number holds
( ( b₂ in c₂ & b₃ in c₃ ) implies ( ( b₂ <= b₁ & b₁ <= b₃ ) ) )

proof

per cases not ( not ( c₂ misses REAL+ & c₃ misses [:{0},REAL+ :] ) & not c₃ meets [:{0},REAL+ :] & not c₂ meets REAL+ ) ;

suppose that E15: c₂ misses REAL+ and
E16: c₃ misses [:{0},REAL+ :] ;

E17: c₃ c= REAL+ by E14, E16, XBOOLE_1:73;
take c₆ = 0;
let c₇, c₈ be real number ;
assume that
E18: c₇ in c₂ and
E19: c₈ in c₃ ;
( not c₆ in [:{0},REAL+ :] & not c₇ in REAL+ ) by E15, E18, ARYTM_0:5, ARYTM_2:21, XBOOLE_0:3;
hence c₇ <= c₆ by E1;
reconsider c₉ = c₈ as Element of REAL+ by E17, E19;
c₁ <=' c₉ by ARYTM_1:6;
hence c₆ <= c₈ by E2;

end;

suppose c₃ meets [:{0},REAL+ :] ;

then consider c₆ being set such that
E15: c₆ in c₃ and
E16: c₆ in [:{0},REAL+ :] by XBOOLE_0:3;
consider c₇, c₈ being set such that
E17: c₇ in {0} and
E18: c₈ in REAL+ and
E19: c₆ = [c₇,c₈] by E16, ZFMISC_1:103;
reconsider c₉ = c₈ as Element of REAL+ by E18;
c₆ in REAL by E15;
then E20: [0,c₉] in REAL by E17, E19, TARSKI:def 1;
then reconsider c₁₀ = [0,c₉] as real number by XREAL_0:def 1;
{ b₁ where B is Element of REAL+ : [0,b₁] in c₃ } c= REAL+

proof

let c₁₁ be set ; :: according to TARSKI:def 3
assume c₁₁ in { b₁ where B is Element of REAL+ : [0,b₁] in c₃ } ;
then ex b₁ being Element of REAL+ st
( c₁₁ = b₁ & [0,b₁] in c₃ ) ;
hence c₁₁ in REAL+ ;

end;

then reconsider c₁₁ = { b₁ where B is Element of REAL+ : [0,b₁] in c₃ } as Subset of REAL+ ;
E21: c₁₀ in [:{0},REAL+ :] by E6, ZFMISC_1:106;
E22: c₁₀ in c₃ by E15, E17, E19, TARSKI:def 1;
then E23: c₉ in c₁₁ ;
E24: c₂ c= [:{0},REAL+ :]

proof

let c₁₂ be set ; :: according to TARSKI:def 3
assume E25: c₁₂ in c₂ ;
then reconsider c₁₃ = c₁₂ as real number by XREAL_0:def 1;

now

assume E26: c₁₃ in REAL+ ;
E27: c₁₃ <= c₁₀ by E7, E22, E25;
( not c₁₀ in REAL+ & not c₁₃ in [:{0},REAL+ :] ) by E21, E26, ARYTM_0:5, XBOOLE_0:3;
hence not verum by E27, E1;

end;

hence c₁₂ in [:{0},REAL+ :] by E13, E25, XBOOLE_0:def 2;

end;

then consider c₁₂, c₁₃ being set such that
E25: c₁₂ in {0} and
E26: c₁₃ in REAL+ and
E27: c₄ = [c₁₂,c₁₃] by E10, ZFMISC_1:103;
reconsider c₁₄ = c₁₃ as Element of REAL+ by E26;
E28: c₄ = [0,c₁₄] by E25, E27, TARSKI:def 1;
{ b₁ where B is Element of REAL+ : [0,b₁] in c₂ } c= REAL+

proof

let c₁₅ be set ; :: according to TARSKI:def 3
assume c₁₅ in { b₁ where B is Element of REAL+ : [0,b₁] in c₂ } ;
then ex b₁ being Element of REAL+ st
( c₁₅ = b₁ & [0,b₁] in c₂ ) ;
hence c₁₅ in REAL+ ;

end;

then reconsider c₁₅ = { b₁ where B is Element of REAL+ : [0,b₁] in c₂ } as Subset of REAL+ ;
E29: c₁₄ in c₁₅ by E10, E28;
for b₁, b₂ being Element of REAL+ holds
( ( b₁ in c₁₁ & b₂ in c₁₅ ) implies ( b₁ <=' b₂ ) )

proof

let c₁₆, c₁₇ be Element of REAL+ ;
assume c₁₆ in c₁₁ ;
then consider c₁₈ being Element of REAL+ such that
E30: c₁₆ = c₁₈ and
E31: [0,c₁₈] in c₃ ;
assume c₁₇ in c₁₅ ;
then consider c₁₉ being Element of REAL+ such that
E32: c₁₇ = c₁₉ and
E33: [0,c₁₉] in c₂ ;
reconsider c₂₀ = [0,c₁₇], c₂₁ = [0,c₁₆] as real number by E30, E31, E32, E33, XREAL_0:def 1;
E34: ( c₂₀ in [:{0},REAL+ :] & c₂₁ in [:{0},REAL+ :] ) by E6, ZFMISC_1:106;
c₂₀ <= c₂₁ by E7, E30, E31, E32, E33;
then consider c₂₂, c₂₃ being Element of REAL+ such that
E35: c₂₀ = [0,c₂₂] and
E36: c₂₁ = [0,c₂₃] and
E37: c₂₃ <=' c₂₂ by E34, E1;
( c₁₇ = c₂₂ & c₁₆ = c₂₃ ) by E35, E36, ZFMISC_1:33;
hence c₁₆ <=' c₁₇ by E37;

end;

then consider c₁₆ being Element of REAL+ such that
E30: for b₁, b₂ being Element of REAL+ holds
( ( b₁ in c₁₁ & b₂ in c₁₅ ) implies ( ( b₁ <=' c₁₆ & c₁₆ <=' b₂ ) ) ) by E23, E29, ARYTM_2:9;
E31: c₉ <> 0 by E20, ARYTM_0:3;
c₉ <=' c₁₆ by E23, E29, E30;
then c₁₆ <> 0 by E31, ARYTM_1:5;
then [0,c₁₆] in REAL by ARYTM_0:2;
then reconsider c₁₇ = [0,c₁₆] as real number by XREAL_0:def 1;
take c₁₇ ;
E32: c₁₇ in [:{0},REAL+ :] by E6, ZFMISC_1:106;
let c₁₈, c₁₉ be real number ;
assume that
E33: c₁₈ in c₂ and
E34: c₁₉ in c₃ ;
consider c₂₀, c₂₁ being set such that
E35: c₂₀ in {0} and
E36: c₂₁ in REAL+ and
E37: c₁₈ = [c₂₀,c₂₁] by E24, E33, ZFMISC_1:103;
reconsider c₂₂ = c₂₁ as Element of REAL+ by E36;
E38: c₁₈ = [0,c₂₂] by E35, E37, TARSKI:def 1;
then E39: c₂₂ in c₁₅ by E33;

now

per cases ( c₁₉ in REAL+ or c₁₉ in [:{0},REAL+ :] ) by E14, E34, XBOOLE_0:def 2;

suppose E40: c₁₉ in REAL+ ;

( c₉ <=' c₁₆ & c₁₆ <=' c₂₂ ) by E23, E30, E39;
hence c₁₈ <= c₁₇ by E24, E32, E33, E38, E2;
( not c₁₇ in REAL+ & not c₁₉ in [:{0},REAL+ :] ) by E32, E40, ARYTM_0:5, XBOOLE_0:3;
hence c₁₇ <= c₁₉ by E1;

end;

suppose E40: c₁₉ in [:{0},REAL+ :] ;

then consider c₂₃, c₂₄ being set such that
E41: c₂₃ in {0} and
E42: c₂₄ in REAL+ and
E43: c₁₉ = [c₂₃,c₂₄] by ZFMISC_1:103;
reconsider c₂₅ = c₂₄ as Element of REAL+ by E42;
E44: c₁₉ = [0,c₂₅] by E41, E43, TARSKI:def 1;
then c₂₅ in c₁₁ by E34;
then ( c₂₅ <=' c₁₆ & c₁₆ <=' c₂₂ ) by E30, E39;
hence ( c₁₈ <= c₁₇ & c₁₇ <= c₁₉ ) by E24, E32, E33, E38, E40, E44, E2;

end;

hence ( c₁₈ <= c₁₇ & c₁₇ <= c₁₉ ) ;

end;

suppose c₂ meets REAL+ ;

then consider c₆ being set such that
E15: c₆ in c₂ and
E16: c₆ in REAL+ by XBOOLE_0:3;
reconsider c₇ = c₆ as Element of REAL+ by E16;
c₇ in REAL+ ;
then reconsider c₈ = c₇ as real number by ARYTM_0:1, XREAL_0:def 1;
reconsider c₉ = c₂ /\ REAL+ as Subset of REAL+ by XBOOLE_1:17;
E17: c₈ in c₉ by E15, XBOOLE_0:def 3;
E18: c₃ c= REAL+

proof

let c₁₀ be set ; :: according to TARSKI:def 3
assume E19: c₁₀ in c₃ ;
then reconsider c₁₁ = c₁₀ as real number by XREAL_0:def 1;

now

assume E20: c₁₁ in [:{0},REAL+ :] ;
E21: c₈ <= c₁₁ by E7, E15, E19;
( not c₁₁ in REAL+ & not c₈ in [:{0},REAL+ :] ) by E20, ARYTM_0:5, XBOOLE_0:3;
hence not verum by E21, E1;

end;

hence c₁₀ in REAL+ by E14, E19, XBOOLE_0:def 2;

end;

then reconsider c₁₀ = c₃ as Subset of REAL+ ;
for b₁, b₂ being Element of REAL+ holds
( ( b₁ in c₉ & b₂ in c₁₀ ) implies ( b₁ <=' b₂ ) )

proof

let c₁₁, c₁₂ be Element of REAL+ ;
assume E19: ( c₁₁ in c₉ & c₁₂ in c₁₀ ) ;
( c₁₁ in REAL+ & c₁₂ in REAL+ ) ;
then reconsider c₁₃ = c₁₁, c₁₄ = c₁₂ as real number by ARYTM_0:1, XREAL_0:def 1;
c₉ c= c₂ by XBOOLE_1:17;
then c₁₃ <= c₁₄ by E7, E19;
then ex b₁, b₂ being Element of REAL+ st
( c₁₃ = b₁ & c₁₄ = b₂ & b₁ <=' b₂ ) by E1;
hence c₁₁ <=' c₁₂ ;

end;

then consider c₁₁ being Element of REAL+ such that
E19: for b₁, b₂ being Element of REAL+ holds
( ( b₁ in c₉ & b₂ in c₁₀ ) implies ( ( b₁ <=' c₁₁ & c₁₁ <=' b₂ ) ) ) by E11, E17, ARYTM_2:9;
c₁₁ in REAL+ ;
then reconsider c₁₂ = c₁₁ as real number by ARYTM_0:1, XREAL_0:def 1;
take c₁₂ ;
let c₁₃, c₁₄ be real number ;
assume that
E20: c₁₃ in c₂ and
E21: c₁₄ in c₃ ;
reconsider c₁₅ = c₁₄ as Element of REAL+ by E18, E21;

now

per cases ( c₁₃ in REAL+ or c₁₃ in [:{0},REAL+ :] ) by E13, E20, XBOOLE_0:def 2;

suppose c₁₃ in REAL+ ;

then reconsider c₁₆ = c₁₃ as Element of REAL+ ;
( c₁₆ in c₉ & c₁₅ in c₁₀ ) by E20, E21, XBOOLE_0:def 3;
then ( c₁₆ <=' c₁₁ & c₁₁ <=' c₁₅ ) by E19;
hence ( c₁₃ <= c₁₂ & c₁₂ <= c₁₄ ) by E2;

end;

suppose c₁₃ in [:{0},REAL+ :] ;

then ( not c₁₃ in REAL+ & not c₁₂ in [:{0},REAL+ :] ) by ARYTM_0:5, XBOOLE_0:3;
hence c₁₃ <= c₁₂ by E1;
( c₇ <=' c₁₁ & c₁₁ <=' c₁₅ ) by E17, E19, E21;
hence c₁₂ <= c₁₄ by E2;

end;

hence ( c₁₃ <= c₁₂ & c₁₂ <= c₁₄ ) ;

end;