let s1, t1, s2, t2 be Real; :: thesis: { |[s,t]| where s, t is Real : ( not s1 <= s or not s <= s2 or not t1 <= t or not t <= t2 ) } = (( { |[s3,t3]| where s3, t3 is Real : s3 < s1 } \/ { |[s4,t4]| where s4, t4 is Real : t4 < t1 } ) \/ { |[s5,t5]| where s5, t5 is Real : s2 < s5 } ) \/ { |[s6,t6]| where s6, t6 is Real : t2 < t6 }
now :: thesis: for x being object st x in { |[s,t]| where s, t is Real : ( not s1 <= s or not s <= s2 or not t1 <= t or not t <= t2 ) } holds
x in (( { |[s3,t3]| where s3, t3 is Real : s3 < s1 } \/ { |[s4,t4]| where s4, t4 is Real : t4 < t1 } ) \/ { |[s5,t5]| where s5, t5 is Real : s2 < s5 } ) \/ { |[s6,t6]| where s6, t6 is Real : t2 < t6 }
let x be object ; :: thesis: ( x in { |[s,t]| where s, t is Real : ( not s1 <= s or not s <= s2 or not t1 <= t or not t <= t2 ) } implies x in (( { |[s3,t3]| where s3, t3 is Real : s3 < s1 } \/ { |[s4,t4]| where s4, t4 is Real : t4 < t1 } ) \/ { |[s5,t5]| where s5, t5 is Real : s2 < s5 } ) \/ { |[s6,t6]| where s6, t6 is Real : t2 < t6 } )
assume x in { |[s,t]| where s, t is Real : ( not s1 <= s or not s <= s2 or not t1 <= t or not t <= t2 ) } ; :: thesis: x in (( { |[s3,t3]| where s3, t3 is Real : s3 < s1 } \/ { |[s4,t4]| where s4, t4 is Real : t4 < t1 } ) \/ { |[s5,t5]| where s5, t5 is Real : s2 < s5 } ) \/ { |[s6,t6]| where s6, t6 is Real : t2 < t6 }
then ex s, t being Real st
( |[s,t]| = x & ( not s1 <= s or not s <= s2 or not t1 <= t or not t <= t2 ) ) ;
then ( x in { |[s3,t3]| where s3, t3 is Real : s3 < s1 } or x in { |[s4,t4]| where s4, t4 is Real : t4 < t1 } or x in { |[s5,t5]| where s5, t5 is Real : s2 < s5 } or x in { |[s6,t6]| where s6, t6 is Real : t2 < t6 } ) ;
then ( x in { |[s3,t3]| where s3, t3 is Real : s3 < s1 } \/ { |[s4,t4]| where s4, t4 is Real : t4 < t1 } or x in { |[s5,t5]| where s5, t5 is Real : s2 < s5 } or x in { |[s6,t6]| where s6, t6 is Real : t2 < t6 } ) by XBOOLE_0:def 3;
then ( x in ( { |[s3,t3]| where s3, t3 is Real : s3 < s1 } \/ { |[s4,t4]| where s4, t4 is Real : t4 < t1 } ) \/ { |[s5,t5]| where s5, t5 is Real : s2 < s5 } or x in { |[s6,t6]| where s6, t6 is Real : t2 < t6 } ) by XBOOLE_0:def 3;
hence x in (( { |[s3,t3]| where s3, t3 is Real : s3 < s1 } \/ { |[s4,t4]| where s4, t4 is Real : t4 < t1 } ) \/ { |[s5,t5]| where s5, t5 is Real : s2 < s5 } ) \/ { |[s6,t6]| where s6, t6 is Real : t2 < t6 } by XBOOLE_0:def 3; :: thesis: verum
end;
then A1: { |[s,t]| where s, t is Real : ( not s1 <= s or not s <= s2 or not t1 <= t or not t <= t2 ) } c= (( { |[s3,t3]| where s3, t3 is Real : s3 < s1 } \/ { |[s4,t4]| where s4, t4 is Real : t4 < t1 } ) \/ { |[s5,t5]| where s5, t5 is Real : s2 < s5 } ) \/ { |[s6,t6]| where s6, t6 is Real : t2 < t6 } ;
now :: thesis: for x being object st x in (( { |[s3,t3]| where s3, t3 is Real : s3 < s1 } \/ { |[s4,t4]| where s4, t4 is Real : t4 < t1 } ) \/ { |[s5,t5]| where s5, t5 is Real : s2 < s5 } ) \/ { |[s6,t6]| where s6, t6 is Real : t2 < t6 } holds
x in { |[s,t]| where s, t is Real : ( not s1 <= s or not s <= s2 or not t1 <= t or not t <= t2 ) }
let x be object ; :: thesis: ( x in (( { |[s3,t3]| where s3, t3 is Real : s3 < s1 } \/ { |[s4,t4]| where s4, t4 is Real : t4 < t1 } ) \/ { |[s5,t5]| where s5, t5 is Real : s2 < s5 } ) \/ { |[s6,t6]| where s6, t6 is Real : t2 < t6 } implies x in { |[s,t]| where s, t is Real : ( not s1 <= s or not s <= s2 or not t1 <= t or not t <= t2 ) } )
assume x in (( { |[s3,t3]| where s3, t3 is Real : s3 < s1 } \/ { |[s4,t4]| where s4, t4 is Real : t4 < t1 } ) \/ { |[s5,t5]| where s5, t5 is Real : s2 < s5 } ) \/ { |[s6,t6]| where s6, t6 is Real : t2 < t6 } ; :: thesis: x in { |[s,t]| where s, t is Real : ( not s1 <= s or not s <= s2 or not t1 <= t or not t <= t2 ) }
then ( x in ( { |[s3,t3]| where s3, t3 is Real : s3 < s1 } \/ { |[s4,t4]| where s4, t4 is Real : t4 < t1 } ) \/ { |[s5,t5]| where s5, t5 is Real : s2 < s5 } or x in { |[s6,t6]| where s6, t6 is Real : t2 < t6 } ) by XBOOLE_0:def 3;
then ( x in { |[s3,t3]| where s3, t3 is Real : s3 < s1 } \/ { |[s4,t4]| where s4, t4 is Real : t4 < t1 } or x in { |[s5,t5]| where s5, t5 is Real : s2 < s5 } or x in { |[s6,t6]| where s6, t6 is Real : t2 < t6 } ) by XBOOLE_0:def 3;
then ( x in { |[s3,t3]| where s3, t3 is Real : s3 < s1 } or x in { |[s4,t4]| where s4, t4 is Real : t4 < t1 } or x in { |[s5,t5]| where s5, t5 is Real : s2 < s5 } or x in { |[s6,t6]| where s6, t6 is Real : t2 < t6 } ) by XBOOLE_0:def 3;
then ( ex sa, ta being Real st
( |[sa,ta]| = x & sa < s1 ) or ex sc, tc being Real st
( |[sc,tc]| = x & tc < t1 ) or ex sb, tb being Real st
( |[sb,tb]| = x & s2 < sb ) or ex sd, td being Real st
( |[sd,td]| = x & t2 < td ) ) ;
hence x in { |[s,t]| where s, t is Real : ( not s1 <= s or not s <= s2 or not t1 <= t or not t <= t2 ) } ; :: thesis: verum
end;
then (( { |[s3,t3]| where s3, t3 is Real : s3 < s1 } \/ { |[s4,t4]| where s4, t4 is Real : t4 < t1 } ) \/ { |[s5,t5]| where s5, t5 is Real : s2 < s5 } ) \/ { |[s6,t6]| where s6, t6 is Real : t2 < t6 } c= { |[s,t]| where s, t is Real : ( not s1 <= s or not s <= s2 or not t1 <= t or not t <= t2 ) } ;
hence { |[s,t]| where s, t is Real : ( not s1 <= s or not s <= s2 or not t1 <= t or not t <= t2 ) } = (( { |[s3,t3]| where s3, t3 is Real : s3 < s1 } \/ { |[s4,t4]| where s4, t4 is Real : t4 < t1 } ) \/ { |[s5,t5]| where s5, t5 is Real : s2 < s5 } ) \/ { |[s6,t6]| where s6, t6 is Real : t2 < t6 } by A1; :: thesis: verum