let X, Y be non empty real-bounded interval 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 object ; :: 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 ;
A6: Y c= [.(lower_bound Y),(upper_bound Y).] by XXREAL_2:69;
then A7: lower_bound Y <= x by A5, XXREAL_1:1;
then A8: lower_bound X <= x by A1, XXREAL_0:2;
A9: x <= upper_bound Y by A5, A6, XXREAL_1:1;
then A10: x <= upper_bound X by A2, XXREAL_0:2;
per cases ( X = [#] REAL or ex a being Real st X = left_closed_halfline a or ex a being Real st X = left_open_halfline a or ex a being Real st X = right_closed_halfline a or ex a being Real st X = right_open_halfline a or ex a, b being Real st
( a <= b & X = [.a,b.] ) or ex a, b being Real st
( a < b & X = [.a,b.[ ) or ex a, b being Real st
( a < b & X = ].a,b.] ) or ex a, b being Real st
( a < b & X = ].a,b.[ ) ) by Th29;
suppose X = [#] REAL ; :: thesis: x in X
hence x in X ; :: thesis: verum
end;
suppose ( ex a being Real st X = left_closed_halfline a or ex a being Real st X = left_open_halfline a or ex a being Real st X = right_closed_halfline a or ex a being Real st X = right_open_halfline a ) ; :: thesis: x in X
hence x in X ; :: thesis: verum
end;
suppose ex a, b being Real st
( a <= b & X = [.a,b.] ) ; :: thesis: x in X
then consider a, b being Real such that
A11: a <= b and
A12: X = [.a,b.] ;
( lower_bound X = a & upper_bound X = b ) by A11, A12, JORDAN5A:19;
hence x in X by A8, A10, A12, XXREAL_1:1; :: thesis: verum
end;
suppose ex a, b being Real st
( a < b & X = [.a,b.[ ) ; :: thesis: x in X
then consider a, b being Real such that
A13: a < b and
A14: X = [.a,b.[ ;
A15: lower_bound X = a by A13, A14, Th4;
A16: upper_bound X = b by A13, A14, Th5;
per cases ( Y = [#] REAL or ex a being Real st Y = left_closed_halfline a or ex a being Real st Y = left_open_halfline a or ex a being Real st Y = right_closed_halfline a or ex a being Real st Y = right_open_halfline a or ex a, b being Real st
( a <= b & Y = [.a,b.] ) or ex a, b being Real st
( a < b & Y = [.a,b.[ ) or ex a, b being Real st
( a < b & Y = ].a,b.] ) or ex a, b being Real st
( a < b & Y = ].a,b.[ ) ) by Th29;
suppose ( ex a being Real st Y = left_closed_halfline a or ex a being Real st Y = left_open_halfline a or ex a being Real st Y = right_closed_halfline a or ex a being Real st Y = right_open_halfline a ) ; :: thesis: x in X
hence x in X ; :: thesis: verum
end;
suppose ex a, b being Real st
( a <= b & Y = [.a,b.] ) ; :: thesis: x in X
then consider a1, b1 being Real such that
A17: ( a1 <= b1 & Y = [.a1,b1.] ) ;
A18: upper_bound Y = b1 by A17, JORDAN5A:19;
then b1 < b by A2, A4, A14, A16, A17, XXREAL_0:1, XXREAL_1:1, XXREAL_1:3;
then x < b by A9, A18, XXREAL_0:2;
hence x in X by A8, A14, A15, XXREAL_1:3; :: thesis: verum
end;
suppose ex a, b being Real st
( a < b & Y = [.a,b.[ ) ; :: thesis: x in X
then consider a1, b1 being Real such that
A19: ( a1 < b1 & Y = [.a1,b1.[ ) ;
( upper_bound Y = b1 & x < b1 ) by A5, A19, Th5, XXREAL_1:3;
then x < b by A2, A16, XXREAL_0:2;
hence x in X by A8, A14, A15, XXREAL_1:3; :: thesis: verum
end;
suppose ex a, b being Real st
( a < b & Y = ].a,b.] ) ; :: thesis: x in X
then consider a1, b1 being Real such that
A20: ( a1 < b1 & Y = ].a1,b1.] ) ;
A21: upper_bound Y = b1 by A20, Th7;
then b1 < b by A2, A4, A14, A16, A20, XXREAL_0:1, XXREAL_1:2, XXREAL_1:3;
then x < b by A9, A21, XXREAL_0:2;
hence x in X by A8, A14, A15, XXREAL_1:3; :: thesis: verum
end;
suppose ex a, b being Real st
( a < b & Y = ].a,b.[ ) ; :: thesis: x in X
then consider a1, b1 being Real such that
A22: ( a1 < b1 & Y = ].a1,b1.[ ) ;
( upper_bound Y = b1 & x < b1 ) by A5, A22, TOPREAL6:17, XXREAL_1:4;
then x < b by A2, A16, XXREAL_0:2;
hence x in X by A8, A14, A15, XXREAL_1:3; :: thesis: verum
end;
end;
end;
suppose ex a, b being Real st
( a < b & X = ].a,b.] ) ; :: thesis: x in X
then consider a, b being Real such that
A23: a < b and
A24: X = ].a,b.] ;
A25: lower_bound X = a by A23, A24, Th6;
A26: upper_bound X = b by A23, A24, Th7;
per cases ( Y = [#] REAL or ex a being Real st Y = left_closed_halfline a or ex a being Real st Y = left_open_halfline a or ex a being Real st Y = right_closed_halfline a or ex a being Real st Y = right_open_halfline a or ex a, b being Real st
( a <= b & Y = [.a,b.] ) or ex a, b being Real st
( a < b & Y = [.a,b.[ ) or ex a, b being Real st
( a < b & Y = ].a,b.] ) or ex a, b being Real st
( a < b & Y = ].a,b.[ ) ) by Th29;
suppose ( ex a being Real st Y = left_closed_halfline a or ex a being Real st Y = left_open_halfline a or ex a being Real st Y = right_closed_halfline a or ex a being Real st Y = right_open_halfline a ) ; :: thesis: x in X
hence x in X ; :: thesis: verum
end;
suppose ex a, b being Real st
( a <= b & Y = [.a,b.] ) ; :: thesis: x in X
then consider a1, b1 being Real such that
A27: ( a1 <= b1 & Y = [.a1,b1.] ) ;
A28: lower_bound Y = a1 by A27, JORDAN5A:19;
then a < a1 by A1, A3, A24, A25, A27, XXREAL_0:1, XXREAL_1:1, XXREAL_1:2;
then a < x by A7, A28, XXREAL_0:2;
hence x in X by A10, A24, A26, XXREAL_1:2; :: thesis: verum
end;
suppose ex a, b being Real st
( a < b & Y = [.a,b.[ ) ; :: thesis: x in X
then consider a1, b1 being Real such that
A29: a1 < b1 and
A30: Y = [.a1,b1.[ ;
lower_bound Y = a1 by A29, A30, Th4;
then A31: a < a1 by A1, A3, A24, A25, A29, A30, XXREAL_0:1, XXREAL_1:2, XXREAL_1:3;
a1 <= x by A5, A30, XXREAL_1:3;
then a < x by A31, XXREAL_0:2;
hence x in X by A10, A24, A26, XXREAL_1:2; :: thesis: verum
end;
suppose ex a, b being Real st
( a < b & Y = ].a,b.] ) ; :: thesis: x in X
then consider a1, b1 being Real such that
A32: ( a1 < b1 & Y = ].a1,b1.] ) ;
( lower_bound Y = a1 & a1 < x ) by A5, A32, Th6, XXREAL_1:2;
then a < x by A1, A25, XXREAL_0:2;
hence x in X by A10, A24, A26, XXREAL_1:2; :: thesis: verum
end;
suppose ex a, b being Real st
( a < b & Y = ].a,b.[ ) ; :: thesis: x in X
then consider a1, b1 being Real such that
A33: ( a1 < b1 & Y = ].a1,b1.[ ) ;
( lower_bound Y = a1 & a1 < x ) by A5, A33, TOPREAL6:17, XXREAL_1:4;
then a < x by A1, A25, XXREAL_0:2;
hence x in X by A10, A24, A26, XXREAL_1:2; :: thesis: verum
end;
end;
end;
suppose ex a, b being Real st
( a < b & X = ].a,b.[ ) ; :: thesis: x in X
then consider a, b being Real such that
A34: a < b and
A35: X = ].a,b.[ ;
A36: lower_bound X = a by A34, A35, TOPREAL6:17;
A37: upper_bound X = b by A34, A35, TOPREAL6:17;
per cases ( Y = [#] REAL or ex a being Real st Y = left_closed_halfline a or ex a being Real st Y = left_open_halfline a or ex a being Real st Y = right_closed_halfline a or ex a being Real st Y = right_open_halfline a or ex a, b being Real st
( a <= b & Y = [.a,b.] ) or ex a, b being Real st
( a < b & Y = [.a,b.[ ) or ex a, b being Real st
( a < b & Y = ].a,b.] ) or ex a, b being Real st
( a < b & Y = ].a,b.[ ) ) by Th29;
suppose ( ex a being Real st Y = left_closed_halfline a or ex a being Real st Y = left_open_halfline a or ex a being Real st Y = right_closed_halfline a or ex a being Real st Y = right_open_halfline a ) ; :: thesis: x in X
hence x in X ; :: thesis: verum
end;
suppose ex a, b being Real st
( a < b & Y = [.a,b.[ ) ; :: thesis: x in X
then consider a1, b1 being Real such that
A43: a1 < b1 and
A44: Y = [.a1,b1.[ ;
lower_bound Y = a1 by A43, A44, Th4;
then A45: a < a1 by A1, A3, A35, A36, A43, A44, XXREAL_0:1, XXREAL_1:3, XXREAL_1:4;
a1 <= x by A5, A44, XXREAL_1:3;
then A46: a < x by A45, XXREAL_0:2;
( upper_bound Y = b1 & x < b1 ) by A5, A43, A44, Th5, XXREAL_1:3;
then x < b by A2, A37, XXREAL_0:2;
hence x in X by A35, A46, XXREAL_1:4; :: thesis: verum
end;
suppose ex a, b being Real st
( a < b & Y = ].a,b.] ) ; :: thesis: x in X
then consider a1, b1 being Real such that
A47: a1 < b1 and
A48: Y = ].a1,b1.] ;
upper_bound Y = b1 by A47, A48, Th7;
then A49: b1 < b by A2, A4, A35, A37, A47, A48, XXREAL_0:1, XXREAL_1:2, XXREAL_1:4;
x <= b1 by A5, A48, XXREAL_1:2;
then A50: x < b by A49, XXREAL_0:2;
( lower_bound Y = a1 & a1 < x ) by A5, A47, A48, Th6, XXREAL_1:2;
then a < x by A1, A36, XXREAL_0:2;
hence x in X by A35, A50, XXREAL_1:4; :: thesis: verum
end;
suppose ex a, b being Real st
( a < b & Y = ].a,b.[ ) ; :: thesis: x in X
then consider a1, b1 being Real such that
A51: ( a1 < b1 & Y = ].a1,b1.[ ) ;
( lower_bound Y = a1 & a1 < x ) by A5, A51, TOPREAL6:17, XXREAL_1:4;
then A52: a < x by A1, A36, XXREAL_0:2;
( upper_bound Y = b1 & x < b1 ) by A5, A51, TOPREAL6:17, XXREAL_1:4;
then x < b by A2, A37, XXREAL_0:2;
hence x in X by A35, A52, XXREAL_1:4; :: thesis: verum
end;
end;
end;
end;