let X be set ; :: thesis: for S being with_empty_element Subset-Family of X holds DIFFERENCE (S,S) = { (A \ B) where A, B is Element of S : verum }
let S be with_empty_element Subset-Family of X; :: thesis: DIFFERENCE (S,S) = { (A \ B) where A, B is Element of S : verum }
thus DIFFERENCE (S,S) c= { (A \ B) where A, B is Element of S : verum } :: according to XBOOLE_0:def 10 :: thesis: { (A \ B) where A, B is Element of S : verum } c= DIFFERENCE (S,S)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in DIFFERENCE (S,S) or x in { (A \ B) where A, B is Element of S : verum } )
assume x in DIFFERENCE (S,S) ; :: thesis: x in { (A \ B) where A, B is Element of S : verum }
then consider X, Y being set such that
A1: ( X in S & Y in S & x = X \ Y ) by SETFAM_1:def 6;
thus x in { (A \ B) where A, B is Element of S : verum } by A1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (A \ B) where A, B is Element of S : verum } or x in DIFFERENCE (S,S) )
assume x in { (A \ B) where A, B is Element of S : verum } ; :: thesis: x in DIFFERENCE (S,S)
then consider A1, B1 being Element of S such that
A2: x = A1 \ B1 ;
thus x in DIFFERENCE (S,S) by A2, SETFAM_1:def 6; :: thesis: verum