let X, Y be set ; :: thesis: ( Y c= X implies X \ (X \ Y) = Y )
assume A1: Y c= X ; :: thesis: X \ (X \ Y) = Y
thus X \ (X \ Y) = X /\ Y by XBOOLE_1:48
.= Y by A1, XBOOLE_1:28 ; :: thesis: verum