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