A _\_ B <> {}

proof

assume A1: A _\_ B = {} ; :: thesis: contradiction
consider A1, A2 being Subset of U such that
A2: ( A1 c= A2 & A = Inter (A1,A2) ) by Th11;
consider B1, B2 being Subset of U such that
A3: ( B1 c= B2 & B = Inter (B1,B2) ) by Th11;
consider y being set such that
A4: y = A1 \ B1 ;
( not A1 in A or not B1 in B or not y = A1 \ B1 ) by A1, SETFAM_1:def 6;
hence contradiction by A4, A2, A3; :: thesis: verum

end;

hence not A _\_ B is empty ; :: thesis: verum