let T be set ; :: thesis: for F being Subset-Family of T st F is compl-closed holds
F = COMPLEMENT F
let F be Subset-Family of T; :: thesis: ( F is compl-closed implies F = COMPLEMENT F )
assume A1: F is compl-closed ; :: thesis: F = COMPLEMENT F
thus F c= COMPLEMENT F :: according to XBOOLE_0:def 10 :: thesis: COMPLEMENT F c= F

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in F or x in COMPLEMENT F )
assume A2: x in F ; :: thesis: x in COMPLEMENT F
then reconsider x9 = x as Subset of T ;
x9 ` in F by A1, A2;
hence x in COMPLEMENT F by SETFAM_1:def 7; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in COMPLEMENT F or x in F )
assume A3: x in COMPLEMENT F ; :: thesis: x in F
then reconsider x9 = x as Subset of T ;
x9 ` in F by A3, SETFAM_1:def 7;
then (x9 `) ` in F by A1;
hence x in F ; :: thesis: verum