let U be non empty set ; 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; 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; ( 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) )
; 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; verum