let X be set ; :: thesis: for F, G being Subset-Family of X st COMPLEMENT F c= COMPLEMENT G holds
F c= G
let F, G be Subset-Family of X; :: thesis: ( COMPLEMENT F c= COMPLEMENT G implies F c= G )
assume A1: COMPLEMENT F c= COMPLEMENT G ; :: thesis: F c= G
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in F or x in G )
assume A2: x in F ; :: thesis: x in G
then reconsider A = x as Subset of X ;
A in COMPLEMENT (COMPLEMENT F) by A2;
then A ` in COMPLEMENT F by Def8;
then (A `) ` in G by A1, Def8;
hence x in G ; :: thesis: verum