take {{} } ; :: thesis: ( not {{} } is empty & {{} } is cup-closed & {{} } is cap-closed & {{} } is diff-closed )
thus not {{} } is empty ; :: thesis: ( {{} } is cup-closed & {{} } is cap-closed & {{} } is diff-closed )
thus {{} } is cup-closed :: thesis: ( {{} } is cap-closed & {{} } is diff-closed )

proof

let X, Y be set ; :: according to FINSUB_1:def 1 :: thesis: ( X in {{} } & Y in {{} } implies X \/ Y in {{} } )
assume ( X in {{} } & Y in {{} } ) ; :: thesis: X \/ Y in {{} }
then ( X = {} & Y = {} ) by TARSKI:def 1;
hence X \/ Y in {{} } by TARSKI:def 1; :: thesis: verum

end;

thus {{} } is cap-closed :: thesis: {{} } is diff-closed

proof

let X, Y be set ; :: according to FINSUB_1:def 2 :: thesis: ( X in {{} } & Y in {{} } implies X /\ Y in {{} } )
assume ( X in {{} } & Y in {{} } ) ; :: thesis: X /\ Y in {{} }
then ( X = {} & Y = {} ) by TARSKI:def 1;
hence X /\ Y in {{} } by TARSKI:def 1; :: thesis: verum

end;

thus {{} } is diff-closed :: thesis: verum

proof

let X, Y be set ; :: according to FINSUB_1:def 3 :: thesis: ( X in {{} } & Y in {{} } implies X \ Y in {{} } )
assume ( X in {{} } & Y in {{} } ) ; :: thesis: X \ Y in {{} }
then ( X = {} & Y = {} ) by TARSKI:def 1;
hence X \ Y in {{} } by TARSKI:def 1; :: thesis: verum

end;