now :: thesis: for A being Subset of X st A in UniCl D holds
A ` in UniCl D

let A be Subset of X; :: thesis: ( A in UniCl D implies A ` in UniCl D )
assume A in UniCl D ; :: thesis: A ` in UniCl D
then A in { (union P) where P is Subset of D : verum } by Th14;
then consider P being Subset of D such that
A1: A = union P ;
reconsider P1 = D \ P as Subset of D by XBOOLE_1:36;
union P1 = (union D) \ (union P) by Th2
.= A ` by A1, EQREL_1:def 4 ;
then A ` in { (union P) where P is Subset of D : verum } ;
hence A ` in UniCl D by Th14; :: thesis: verum

end;

hence UniCl D is compl-closed ; :: thesis: verum