let U be non empty set ; :: thesis: for A, C being non empty IntervalSet of U
for X, Y being Subset of U st A = Inter X,Y holds
A _\_ C = Inter (X \ (C ``2 )),(Y \ (C ``1 ))
let A, C be non empty IntervalSet of U; :: thesis: for X, Y being Subset of U st A = Inter X,Y holds
A _\_ C = Inter (X \ (C ``2 )),(Y \ (C ``1 ))
let X, Y be Subset of U; :: thesis: ( A = Inter X,Y implies A _\_ C = Inter (X \ (C ``2 )),(Y \ (C ``1 )) )
assume a0: A = Inter X,Y ; :: thesis: A _\_ C = Inter (X \ (C ``2 )),(Y \ (C ``1 ))
A = Inter (A ``1 ),(A ``2 ) by Wazne33;
then ( X = A ``1 & Y = A ``2 ) by a0, Pik;
hence A _\_ C = Inter (X \ (C ``2 )),(Y \ (C ``1 )) by Dif; :: thesis: verum