let X be set ; :: thesis: for S being with_empty_element cap-closed semi-diff-closed Subset-Family of X
for A, B being set st A in S & B in S holds
B \ A in DisUnion S
let S be with_empty_element cap-closed semi-diff-closed Subset-Family of X; :: thesis: for A, B being set st A in S & B in S holds
B \ A in DisUnion S
let A, B be set ; :: thesis: ( A in S & B in S implies B \ A in DisUnion S )
assume A2: ( A in S & B in S ) ; :: thesis: B \ A in DisUnion S
reconsider A1 = A, B1 = B as Subset of X by A2;
ex F being disjoint_valued FinSequence of S st B \ A = Union F by A2, DefSD;
then B1 \ A1 in DisUnion S ;
hence B \ A in DisUnion S ; :: thesis: verum