SCM-Data-Loc misses {NAT} by AMI_2:27, ZFMISC_1:56;
then A1: SCM-Data-Loc misses {NAT} \/ NAT by AMI_2:29, XBOOLE_1:70;
thus Data-Locations SCM = (({NAT} \/ SCM-Data-Loc) \/ NAT) \ ({NAT} \/ NAT) by AMI_2:30, FUNCT_7:def 1
.= (SCM-Data-Loc \/ ({NAT} \/ NAT)) \ ({NAT} \/ NAT) by XBOOLE_1:4
.= SCM-Data-Loc \ ({NAT} \/ NAT) by XBOOLE_1:40
.= SCM-Data-Loc by A1, XBOOLE_1:83 ; :: thesis: verum