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

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