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 that
A1: X in {{} } and
A2: Y in {{} } ; :: thesis: X \/ Y in {{} }
X = {} by A1, TARSKI:def 1;
hence X \/ Y in {{} } by A2; :: 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 that
A3: X in {{} } and
Y in {{} } ; :: thesis: X /\ Y in {{} }
X = {} by A3, 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 that
A4: X in {{} } and
Y in {{} } ; :: thesis: X \ Y in {{} }
X = {} by A4, TARSKI:def 1;
hence X \ Y in {{} } by TARSKI:def 1; :: thesis: verum

end;