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 )

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

hence
COMPLEMENT F = {{}}
by Def7; :: thesis: verum
let P be Subset of X; :: thesis: ( P in G iff P ` in F )

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;hereby :: thesis: ( P ` in F implies P in G )

assume
P ` in F
; :: thesis: P in Gassume
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;then P = {} X by TARSKI:def 1;

hence P ` in F by A1, TARSKI:def 1; :: thesis: verum

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