A _\_ B <> {}

proof

hence
not A _\_ B is empty
; :: thesis: verum
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;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