let X, Y, Z be set ; :: thesis: ( 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 & union {Z} = Z ) by ZFMISC_1:31, ZFMISC_1:93, ZFMISC_1:96;
A2: ( meet ({X,Y} \/ {Z}) = (meet {X,Y}) /\ (meet {Z}) & meet {X,Y} = X /\ Y & meet {Z} = Z ) by SETFAM_1:10, SETFAM_1:11, SETFAM_1:12;
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, A3, FINSEQ_2:148 ; :: thesis: meet <*X,Y,Z*> = (X /\ Y) /\ Z
thus meet <*X,Y,Z*> = (X /\ Y) /\ Z by A2, A3, FINSEQ_2:148; :: thesis: verum