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

let A, B be Subset-Family of U; :: thesis: DIFFERENCE (A,B) is Subset-Family of U

DIFFERENCE (A,B) c= bool U

proof

hence
DIFFERENCE (A,B) is Subset-Family of U
; :: thesis: verum
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;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