now :: thesis: for SF being Subset-Family of X st SF is union-closed holds
SF is cup-closed

let SF be Subset-Family of X; :: thesis: ( SF is union-closed implies SF is cup-closed )
assume A1: SF is union-closed ; :: thesis: SF is cup-closed

now :: thesis: for a, b being set st a in SF & b in SF holds
a \/ b in SF

let a, b be set ; :: thesis: ( a in SF & b in SF implies a \/ b in SF )
assume that
A2: a in SF and
A3: b in SF ; :: thesis: a \/ b in SF
A4: {a,b} c= SF by A2, A3, TARSKI:def 2;
SF c= bool X ;
then {a,b} c= bool X by A4;
then reconsider c = {a,b} as Subset-Family of X ;
{a,b} c= SF by A2, A3, TARSKI:def 2;
then union c in SF by A1;
hence a \/ b in SF by ZFMISC_1:75; :: thesis: verum

end;

hence SF is cup-closed ; :: thesis: verum

end;

hence for b₁ being Subset-Family of X st b₁ is union-closed holds
b₁ is cup-closed ; :: thesis: verum