{{}} /\ (Fin S) = {{}}

proof

thus {{}} /\ (Fin S) c= {{}} by XBOOLE_1:17; :: according to XBOOLE_0:def 10 :: thesis: {{}} c= {{}} /\ (Fin S)
{{}} c= Fin S

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {{}} or x in Fin S )
assume x in {{}} ; :: thesis: x in Fin S
then J1: x = {} by TARSKI:def 1;
( {} c= S & {} is finite ) by XBOOLE_1:2;
hence x in Fin S by J1, FINSUB_1:def 5; :: thesis: verum

end;

hence {{}} c= {{}} /\ (Fin S) by XBOOLE_1:19; :: thesis: verum

end;

hence union ((PARTITIONS {}) /\ (Fin S)) is empty by A4bis; :: thesis: verum