let m, n be Nat; :: thesis: [:(NAT \ (Segm m)),(NAT \ (Segm n)):] c= [:NAT,NAT:] \ [:(Segm m),(Segm n):]
A1: [:NAT,NAT:] \ [:(Segm m),(Segm n):] = [:(NAT \ (Segm m)),NAT:] \/ [:NAT,(NAT \ (Segm n)):] by ZFMISC_1:103;
[:(NAT \ (Segm m)),(NAT \ (Segm n)):] = [:(NAT \ (Segm m)),NAT:] \ [:(NAT \ (Segm m)),(Segm n):] by ZFMISC_1:102;
hence [:(NAT \ (Segm m)),(NAT \ (Segm n)):] c= [:NAT,NAT:] \ [:(Segm m),(Segm n):] by A1, XBOOLE_1:10; :: thesis: verum