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 a0: ( 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 Wazne33;
then ( A ``1 = X & A ``2 = Y & C ``1 = W & C ``2 = Z ) by a0, Pik;
hence A _\_ C = Inter (X \ Z),(Y \ W) by Dif; :: thesis: verum