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 ;
then reconsider G = {{}} as Subset-Family of X by ZFMISC_1:31;
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 Def7; :: thesis: verum