let a, b be Ordinal; :: thesis: for x being set holds
( x in a \ b iff ( b c= x & x in a ) )
let x be set ; :: thesis: ( x in a \ b iff ( b c= x & x in a ) )
( x in a \ b iff ( x nin b & x in a ) ) by XBOOLE_0:def 5;
hence ( x in a \ b iff ( b c= x & x in a ) ) by Th4; :: thesis: verum