let X be set ; :: thesis: for L1, L2 being List of X holds ROUGH (<*L1,L2*>,2) = L1 AND L2
let L1, L2 be List of X; :: thesis: ROUGH (<*L1,L2*>,2) = L1 AND L2
( len <*L1,L2*> = 2 & rng <*L1,L2*> = {L1,L2} & meet {L1,L2} = L1 AND L2 ) by FINSEQ_1:44, FINSEQ_2:127, SETFAM_1:11;
hence ROUGH (<*L1,L2*>,2) = L1 AND L2 by Th62; :: thesis: verum