let X, Y, Z be set ; ( Union <*X,Y,Z*> = (X \/ Y) \/ Z & meet <*X,Y,Z*> = (X /\ Y) /\ Z )
A1:
( union ({X,Y} \/ {Z}) = (union {X,Y}) \/ (union {Z}) & union {X,Y} = X \/ Y )
by ZFMISC_1:93, ZFMISC_1:96;
A2:
union {Z} = Z
by ZFMISC_1:31;
A3:
{X,Y} \/ {Z} = {X,Y,Z}
by ENUMSET1:43;
thus Union <*X,Y,Z*> =
union (rng <*X,Y,Z*>)
by CARD_3:def 4
.=
(X \/ Y) \/ Z
by A1, A2, A3, FINSEQ_2:148
; meet <*X,Y,Z*> = (X /\ Y) /\ Z
A4:
meet {Z} = Z
by SETFAM_1:11;
( meet ({X,Y} \/ {Z}) = (meet {X,Y}) /\ (meet {Z}) & meet {X,Y} = X /\ Y )
by SETFAM_1:10, SETFAM_1:12;
hence
meet <*X,Y,Z*> = (X /\ Y) /\ Z
by A4, A3, FINSEQ_2:148; verum