let T be set ; :: thesis: for F, G being Subset-Family of T st F c= G & G is compl-closed holds

COMPLEMENT F c= G

let F, G be Subset-Family of T; :: thesis: ( F c= G & G is compl-closed implies COMPLEMENT F c= G )

assume A1: ( F c= G & G is compl-closed ) ; :: thesis: COMPLEMENT F c= G

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in COMPLEMENT F or x in G )

assume A2: x in COMPLEMENT F ; :: thesis: x in G

then reconsider x9 = x as Subset of T ;

x9 ` in F by A2, SETFAM_1:def 7;

then (x9 `) ` in G by A1;

hence x in G ; :: thesis: verum

COMPLEMENT F c= G

let F, G be Subset-Family of T; :: thesis: ( F c= G & G is compl-closed implies COMPLEMENT F c= G )

assume A1: ( F c= G & G is compl-closed ) ; :: thesis: COMPLEMENT F c= G

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in COMPLEMENT F or x in G )

assume A2: x in COMPLEMENT F ; :: thesis: x in G

then reconsider x9 = x as Subset of T ;

x9 ` in F by A2, SETFAM_1:def 7;

then (x9 `) ` in G by A1;

hence x in G ; :: thesis: verum