let X be set ; 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; 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 }
XBOOLE_0:def 10 { (A \ B) where A, B is Element of S : verum } c= DIFFERENCE (S,S)
let x be object ; TARSKI:def 3 ( 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 }
; 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; verum