let E be set ; :: thesis: for A being Subset of E holds A \/ (A `) = [#] E
let A be Subset of E; :: thesis: A \/ (A `) = [#] E
A in bool E by Def1;
then A c= E by ZFMISC_1:def 1;
hence A \/ (A `) = [#] E by XBOOLE_1:45; :: thesis: verum