let n be Element of NAT ; :: thesis: for X, Y, Z being Subset of (TOP-REAL n) holds X (-) (Y (+) Z) = (X (-) Z) (-) Y
let X, Y, Z be Subset of (TOP-REAL n); :: thesis: X (-) (Y (+) Z) = (X (-) Z) (-) Y
X (-) (Y (+) Z) = X (-) (Z (+) Y) by Th12
.= (X (-) Z) (-) Y by Th23 ;
hence X (-) (Y (+) Z) = (X (-) Z) (-) Y ; :: thesis: verum