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;