let A, B, X be set ; :: thesis: ( X c= A \ B implies ( X c= A & X misses B ) )
assume A1: X c= A \ B ; :: thesis: ( X c= A & X misses B )
A \ B c= A by Th36;
hence X c= A by A1; :: thesis: X misses B
now :: thesis: for x being object st x in X holds
not x in B
let x be object ; :: thesis: ( x in X implies not x in B )
assume x in X ; :: thesis: not x in B
then x in A \ B by A1;
hence not x in B by XBOOLE_0:def 5; :: thesis: verum
end;
hence X misses B by XBOOLE_0:3; :: thesis: verum