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

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

hence
X misses B
by XBOOLE_0:3; :: thesis: verumnot 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;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