let X be set ; :: thesis: for F being Subset-Family of X st F = {X} holds
COMPLEMENT F = {{} }
let F be Subset-Family of X; :: thesis: ( F = {X} implies COMPLEMENT F = {{} } )
assume A1: F = {X} ; :: thesis: COMPLEMENT F = {{} }
{} c= X by XBOOLE_1:2;
then reconsider G = {{} } as Subset-Family of X by ZFMISC_1:37;
reconsider G = G as Subset-Family of X ;
for P being Subset of X holds
( P in G iff P ` in F )

proof

let P be Subset of X; :: thesis: ( P in G iff P ` in F )

hereby :: thesis: ( P ` in F implies P in G )

assume P in G ; :: thesis: P ` in F
then P = {} X by TARSKI:def 1;
hence P ` in F by A1, TARSKI:def 1; :: thesis: verum

end;

assume P ` in F ; :: thesis: P in G
then A2: P ` = [#] X by A1, TARSKI:def 1;
P = (P ` ) `
.= {} by A2, XBOOLE_1:37 ;
hence P in G by TARSKI:def 1; :: thesis: verum

end;

hence COMPLEMENT F = {{} } by Def8; :: thesis: verum