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