A _\_ B <> {}
proof
assume Q1:
A _\_ B = {}
;
contradiction
consider A1,
A2 being
Subset of
U such that p1:
(
A1 c= A2 &
A = Inter (
A1,
A2) )
by U2;
consider B1,
B2 being
Subset of
U such that p2:
(
B1 c= B2 &
B = Inter (
B1,
B2) )
by U2;
consider y being
set such that q4:
y = A1 \ B1
;
( not
A1 in A or not
B1 in B or not
y = A1 \ B1 )
by SETFAM_1:def 6, Q1;
hence
contradiction
by q4, p1, p2;
verum
end;
hence
not A _\_ B is empty
; verum