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

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