let S, T be Subset of E; :: thesis: ( S = E \ T implies T = E \ S )
assume A1: S = E \ T ; :: thesis: T = E \ S
T in bool E by Def1;
then T c= E by ZFMISC_1:def 1;
hence T = {} \/ (E /\ T) by XBOOLE_1:28
.= (E \ E) \/ (E /\ T) by XBOOLE_1:37
.= E \ S by A1, XBOOLE_1:52 ;
:: thesis: verum