let X be set ; :: thesis: for F, G being Subset-Family of X holds
( COMPLEMENT F c= G iff F c= COMPLEMENT G )
let F, G be Subset-Family of X; :: thesis: ( COMPLEMENT F c= G iff F c= COMPLEMENT G )

hereby :: thesis: ( F c= COMPLEMENT G implies COMPLEMENT F c= G )

assume COMPLEMENT F c= G ; :: thesis: F c= COMPLEMENT G
then COMPLEMENT F c= COMPLEMENT (COMPLEMENT G) ;
hence F c= COMPLEMENT G by Th36; :: thesis: verum

end;

assume F c= COMPLEMENT G ; :: thesis: COMPLEMENT F c= G
then COMPLEMENT (COMPLEMENT F) c= COMPLEMENT G ;
hence COMPLEMENT F c= G by Th36; :: thesis: verum