let X, Y be set ; :: thesis: ( Union <*X,Y*> = X \/ Y & meet <*X,Y*> = X /\ Y )
thus Union <*X,Y*> = union (rng <*X,Y*>)
.= union {X,Y} by FINSEQ_2:127
.= X \/ Y by ZFMISC_1:75 ; :: thesis: meet <*X,Y*> = X /\ Y
thus meet <*X,Y*> = meet {X,Y} by FINSEQ_2:127
.= X /\ Y by SETFAM_1:11 ; :: thesis: verum