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:75, ZFMISC_1:78;
A2:
union {Z} = Z
by ZFMISC_1:25;
A3:
{X,Y} \/ {Z} = {X,Y,Z}
by ENUMSET1:3;
thus Union <*X,Y,Z*> =
union (rng <*X,Y,Z*>)
.=
(X \/ Y) \/ Z
by A1, A2, A3, FINSEQ_2:128
; meet <*X,Y,Z*> = (X /\ Y) /\ Z
A4:
meet {Z} = Z
by SETFAM_1:10;
( meet ({X,Y} \/ {Z}) = (meet {X,Y}) /\ (meet {Z}) & meet {X,Y} = X /\ Y )
by SETFAM_1:9, SETFAM_1:11;
hence
meet <*X,Y,Z*> = (X /\ Y) /\ Z
by A4, A3, FINSEQ_2:128; verum