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

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