let X, Y be non empty bounded connected Subset of REAL ; :: thesis: ( lower_bound X <= lower_bound Y & upper_bound Y <= upper_bound X & ( lower_bound X = lower_bound Y & lower_bound Y in Y implies lower_bound X in X ) & ( upper_bound X = upper_bound Y & upper_bound Y in Y implies upper_bound X in X ) implies Y c= X )
assume that
A1: lower_bound X <= lower_bound Y and
A2: upper_bound Y <= upper_bound X and
A3: ( lower_bound X = lower_bound Y & lower_bound Y in Y implies lower_bound X in X ) and
A4: ( upper_bound X = upper_bound Y & upper_bound Y in Y implies upper_bound X in X ) ; :: thesis: Y c= X
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Y or x in X )
assume A5: x in Y ; :: thesis: x in X
then reconsider x = x as Real ;
Y c= [.(lower_bound Y),(upper_bound Y).] by TOPREAL6:24;
then A6: ( lower_bound Y <= x & x <= upper_bound Y ) by A5, XXREAL_1:1;
then A7: ( lower_bound X <= x & x <= upper_bound X ) by A1, A2, XXREAL_0:2;
per cases ( X = [#] REAL or ex a being real number st X = left_closed_halfline a or ex a being real number st X = left_open_halfline a or ex a being real number st X = right_closed_halfline a or ex a being real number st X = right_open_halfline a or ex a, b being real number st
( a <= b & X = [.a,b.] ) or ex a, b being real number st
( a < b & X = [.a,b.[ ) or ex a, b being real number st
( a < b & X = ].a,b.] ) or ex a, b being real number st
( a < b & X = ].a,b.[ ) ) by Th41;
suppose X = [#] REAL ; :: thesis: x in X
hence x in X ; :: thesis: verum
end;
suppose ( ex a being real number st X = left_closed_halfline a or ex a being real number st X = left_open_halfline a or ex a being real number st X = right_closed_halfline a or ex a being real number st X = right_open_halfline a ) ; :: thesis: x in X
hence x in X ; :: thesis: verum
end;
suppose ex a, b being real number st
( a <= b & X = [.a,b.] ) ; :: thesis: x in X
then consider a, b being real number such that
A8: ( a <= b & X = [.a,b.] ) ;
( lower_bound X = a & upper_bound X = b ) by A8, JORDAN5A:20;
hence x in X by A7, A8, XXREAL_1:1; :: thesis: verum
end;
suppose ex a, b being real number st
( a < b & X = [.a,b.[ ) ; :: thesis: x in X
then consider a, b being real number such that
A9: ( a < b & X = [.a,b.[ ) ;
A10: ( lower_bound X = a & upper_bound X = b ) by A9, Th4, Th5;
per cases ( Y = [#] REAL or ex a being real number st Y = left_closed_halfline a or ex a being real number st Y = left_open_halfline a or ex a being real number st Y = right_closed_halfline a or ex a being real number st Y = right_open_halfline a or ex a, b being real number st
( a <= b & Y = [.a,b.] ) or ex a, b being real number st
( a < b & Y = [.a,b.[ ) or ex a, b being real number st
( a < b & Y = ].a,b.] ) or ex a, b being real number st
( a < b & Y = ].a,b.[ ) ) by Th41;
suppose ex a, b being real number st
( a <= b & Y = [.a,b.] ) ; :: thesis: x in X
then consider a1, b1 being real number such that
A11: ( a1 <= b1 & Y = [.a1,b1.] ) ;
A12: ( lower_bound Y = a1 & upper_bound Y = b1 ) by A11, JORDAN5A:20;
then b1 < b by A2, A4, A9, A10, A11, XXREAL_0:1, XXREAL_1:1, XXREAL_1:3;
then x < b by A6, A12, XXREAL_0:2;
hence x in X by A7, A9, A10, XXREAL_1:3; :: thesis: verum
end;
suppose ex a, b being real number st
( a < b & Y = [.a,b.[ ) ; :: thesis: x in X
then consider a1, b1 being real number such that
A13: ( a1 < b1 & Y = [.a1,b1.[ ) ;
A14: ( lower_bound Y = a1 & upper_bound Y = b1 ) by A13, Th4, Th5;
x < b1 by A5, A13, XXREAL_1:3;
then x < b by A2, A10, A14, XXREAL_0:2;
hence x in X by A7, A9, A10, XXREAL_1:3; :: thesis: verum
end;
suppose ex a, b being real number st
( a < b & Y = ].a,b.] ) ; :: thesis: x in X
then consider a1, b1 being real number such that
A15: ( a1 < b1 & Y = ].a1,b1.] ) ;
A16: ( lower_bound Y = a1 & upper_bound Y = b1 ) by A15, Th6, Th7;
then b1 < b by A2, A4, A9, A10, A15, XXREAL_0:1, XXREAL_1:2, XXREAL_1:3;
then x < b by A6, A16, XXREAL_0:2;
hence x in X by A7, A9, A10, XXREAL_1:3; :: thesis: verum
end;
suppose ex a, b being real number st
( a < b & Y = ].a,b.[ ) ; :: thesis: x in X
then consider a1, b1 being real number such that
A17: ( a1 < b1 & Y = ].a1,b1.[ ) ;
A18: ( lower_bound Y = a1 & upper_bound Y = b1 ) by A17, TOPREAL6:22;
x < b1 by A5, A17, XXREAL_1:4;
then x < b by A2, A10, A18, XXREAL_0:2;
hence x in X by A7, A9, A10, XXREAL_1:3; :: thesis: verum
end;
end;
end;
suppose ex a, b being real number st
( a < b & X = ].a,b.] ) ; :: thesis: x in X
then consider a, b being real number such that
A19: ( a < b & X = ].a,b.] ) ;
A20: ( lower_bound X = a & upper_bound X = b ) by A19, Th6, Th7;
per cases ( Y = [#] REAL or ex a being real number st Y = left_closed_halfline a or ex a being real number st Y = left_open_halfline a or ex a being real number st Y = right_closed_halfline a or ex a being real number st Y = right_open_halfline a or ex a, b being real number st
( a <= b & Y = [.a,b.] ) or ex a, b being real number st
( a < b & Y = [.a,b.[ ) or ex a, b being real number st
( a < b & Y = ].a,b.] ) or ex a, b being real number st
( a < b & Y = ].a,b.[ ) ) by Th41;
suppose ex a, b being real number st
( a <= b & Y = [.a,b.] ) ; :: thesis: x in X
then consider a1, b1 being real number such that
A21: ( a1 <= b1 & Y = [.a1,b1.] ) ;
A22: ( lower_bound Y = a1 & upper_bound Y = b1 ) by A21, JORDAN5A:20;
then a < a1 by A1, A3, A19, A20, A21, XXREAL_0:1, XXREAL_1:1, XXREAL_1:2;
then a < x by A6, A22, XXREAL_0:2;
hence x in X by A7, A19, A20, XXREAL_1:2; :: thesis: verum
end;
suppose ex a, b being real number st
( a < b & Y = [.a,b.[ ) ; :: thesis: x in X
then consider a1, b1 being real number such that
A23: ( a1 < b1 & Y = [.a1,b1.[ ) ;
( lower_bound Y = a1 & upper_bound Y = b1 ) by A23, Th4, Th5;
then A24: a < a1 by A1, A3, A19, A20, A23, XXREAL_0:1, XXREAL_1:2, XXREAL_1:3;
a1 <= x by A5, A23, XXREAL_1:3;
then a < x by A24, XXREAL_0:2;
hence x in X by A7, A19, A20, XXREAL_1:2; :: thesis: verum
end;
suppose ex a, b being real number st
( a < b & Y = ].a,b.] ) ; :: thesis: x in X
then consider a1, b1 being real number such that
A25: ( a1 < b1 & Y = ].a1,b1.] ) ;
A26: ( lower_bound Y = a1 & upper_bound Y = b1 ) by A25, Th6, Th7;
a1 < x by A5, A25, XXREAL_1:2;
then a < x by A1, A20, A26, XXREAL_0:2;
hence x in X by A7, A19, A20, XXREAL_1:2; :: thesis: verum
end;
suppose ex a, b being real number st
( a < b & Y = ].a,b.[ ) ; :: thesis: x in X
then consider a1, b1 being real number such that
A27: ( a1 < b1 & Y = ].a1,b1.[ ) ;
A28: ( lower_bound Y = a1 & upper_bound Y = b1 ) by A27, TOPREAL6:22;
a1 < x by A5, A27, XXREAL_1:4;
then a < x by A1, A20, A28, XXREAL_0:2;
hence x in X by A7, A19, A20, XXREAL_1:2; :: thesis: verum
end;
end;
end;
suppose ex a, b being real number st
( a < b & X = ].a,b.[ ) ; :: thesis: x in X
then consider a, b being real number such that
A29: ( a < b & X = ].a,b.[ ) ;
A30: ( lower_bound X = a & upper_bound X = b ) by A29, TOPREAL6:22;
per cases ( Y = [#] REAL or ex a being real number st Y = left_closed_halfline a or ex a being real number st Y = left_open_halfline a or ex a being real number st Y = right_closed_halfline a or ex a being real number st Y = right_open_halfline a or ex a, b being real number st
( a <= b & Y = [.a,b.] ) or ex a, b being real number st
( a < b & Y = [.a,b.[ ) or ex a, b being real number st
( a < b & Y = ].a,b.] ) or ex a, b being real number st
( a < b & Y = ].a,b.[ ) ) by Th41;
suppose ex a, b being real number st
( a < b & Y = [.a,b.[ ) ; :: thesis: x in X
then consider a1, b1 being real number such that
A35: ( a1 < b1 & Y = [.a1,b1.[ ) ;
A36: ( lower_bound Y = a1 & upper_bound Y = b1 ) by A35, Th4, Th5;
x < b1 by A5, A35, XXREAL_1:3;
then A37: x < b by A2, A30, A36, XXREAL_0:2;
A38: a < a1 by A1, A3, A29, A30, A35, A36, XXREAL_0:1, XXREAL_1:3, XXREAL_1:4;
a1 <= x by A5, A35, XXREAL_1:3;
then a < x by A38, XXREAL_0:2;
hence x in X by A29, A37, XXREAL_1:4; :: thesis: verum
end;
suppose ex a, b being real number st
( a < b & Y = ].a,b.] ) ; :: thesis: x in X
then consider a1, b1 being real number such that
A39: ( a1 < b1 & Y = ].a1,b1.] ) ;
A40: ( lower_bound Y = a1 & upper_bound Y = b1 ) by A39, Th6, Th7;
A41: x <= b1 by A5, A39, XXREAL_1:2;
b1 < b by A2, A4, A29, A30, A39, A40, XXREAL_0:1, XXREAL_1:2, XXREAL_1:4;
then A42: x < b by A41, XXREAL_0:2;
a1 < x by A5, A39, XXREAL_1:2;
then a < x by A1, A30, A40, XXREAL_0:2;
hence x in X by A29, A42, XXREAL_1:4; :: thesis: verum
end;
suppose ex a, b being real number st
( a < b & Y = ].a,b.[ ) ; :: thesis: x in X
then consider a1, b1 being real number such that
A43: ( a1 < b1 & Y = ].a1,b1.[ ) ;
A44: ( lower_bound Y = a1 & upper_bound Y = b1 ) by A43, TOPREAL6:22;
x < b1 by A5, A43, XXREAL_1:4;
then A45: x < b by A2, A30, A44, XXREAL_0:2;
a1 < x by A5, A43, XXREAL_1:4;
then a < x by A1, A30, A44, XXREAL_0:2;
hence x in X by A29, A45, XXREAL_1:4; :: thesis: verum
end;
end;
end;
end;