let X, Y be set ; :: thesis: ( Union <*X,Y*> = X \/ Y & meet <*X,Y*> = X /\ Y )
thus Union <*X,Y*> = union (rng <*X,Y*>) by CARD_3:def 4
.= union {X,Y} by FINSEQ_2:147
.= X \/ Y by ZFMISC_1:93 ; :: thesis: meet <*X,Y*> = X /\ Y
thus meet <*X,Y*> = meet {X,Y} by FINSEQ_2:147
.= X /\ Y by SETFAM_1:12 ; :: thesis: verum