let X be set ; :: thesis: for L1, L2 being List of X holds ROUGH (<*L1,L2*>,1) = L1 OR L2

let L1, L2 be List of X; :: thesis: ROUGH (<*L1,L2*>,1) = L1 OR L2

( len <*L1,L2*> = 2 & rng <*L1,L2*> = {L1,L2} & union {L1,L2} = L1 OR L2 & Union <*L1,L2*> = union (rng <*L1,L2*>) ) by CARD_3:def 4, FINSEQ_1:44, FINSEQ_2:127, ZFMISC_1:75;

hence ROUGH (<*L1,L2*>,1) = L1 OR L2 by Th63; :: thesis: verum

let L1, L2 be List of X; :: thesis: ROUGH (<*L1,L2*>,1) = L1 OR L2

( len <*L1,L2*> = 2 & rng <*L1,L2*> = {L1,L2} & union {L1,L2} = L1 OR L2 & Union <*L1,L2*> = union (rng <*L1,L2*>) ) by CARD_3:def 4, FINSEQ_1:44, FINSEQ_2:127, ZFMISC_1:75;

hence ROUGH (<*L1,L2*>,1) = L1 OR L2 by Th63; :: thesis: verum