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 A1: A = Inter (X,Y) ; :: thesis: A _\_ C = Inter ((X \ (C ``2)),(Y \ (C ``1)))
A = Inter ((A ``1),(A ``2)) by Th15;
then ( X = A ``1 & Y = A ``2 ) by A1, Th6;
hence A _\_ C = Inter ((X \ (C ``2)),(Y \ (C ``1))) by Th40; :: thesis: verum