let X be set ; :: thesis: for F, G being Subset-Family of X st COMPLEMENT F = COMPLEMENT G holds
F = G
let F, G be Subset-Family of X; :: thesis: ( COMPLEMENT F = COMPLEMENT G implies F = G )
assume COMPLEMENT F = COMPLEMENT G ; :: thesis: F = G
hence F = COMPLEMENT (COMPLEMENT G)
.= G ;
:: thesis: verum