let U be non empty set ; :: thesis: for A, C being non empty IntervalSet of U
for X, Y, W, Z being Subset of U st A = Inter (X,Y) & C = Inter (W,Z) holds
A _\_ C = Inter ((X \ Z),(Y \ W))
let A, C be non empty IntervalSet of U; :: thesis: for X, Y, W, Z being Subset of U st A = Inter (X,Y) & C = Inter (W,Z) holds
A _\_ C = Inter ((X \ Z),(Y \ W))
let X, Y, W, Z be Subset of U; :: thesis: ( A = Inter (X,Y) & C = Inter (W,Z) implies A _\_ C = Inter ((X \ Z),(Y \ W)) )
assume A1: ( A = Inter (X,Y) & C = Inter (W,Z) ) ; :: thesis: A _\_ C = Inter ((X \ Z),(Y \ W))
( A = Inter ((A ``1),(A ``2)) & C = Inter ((C ``1),(C ``2)) ) by Th15;
then ( A ``1 = X & A ``2 = Y & C ``1 = W & C ``2 = Z ) by A1, Th6;
hence A _\_ C = Inter ((X \ Z),(Y \ W)) by Th40; :: thesis: verum