let U be non empty set ; :: thesis: for A, B being Subset-Family of U holds DIFFERENCE (A,B) is Subset-Family of U
let A, B be Subset-Family of U; :: thesis: DIFFERENCE (A,B) is Subset-Family of U
DIFFERENCE (A,B) c= bool U
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in DIFFERENCE (A,B) or x in bool U )
assume x in DIFFERENCE (A,B) ; :: thesis: x in bool U
then consider Y, Z being set such that
A1: ( Y in A & Z in B & x = Y \ Z ) by SETFAM_1:def 6;
Y \ Z c= U by A1, XBOOLE_1:109;
hence x in bool U by A1; :: thesis: verum
end;
hence DIFFERENCE (A,B) is Subset-Family of U ; :: thesis: verum