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 object ; :: 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 Def7;

then (A `) ` in G by A1, Def7;

hence x in G ; :: thesis: verum

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 object ; :: 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 Def7;

then (A `) ` in G by A1, Def7;

hence x in G ; :: thesis: verum