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

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

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 COMPLEMENT F or x in F )
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;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

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