SCM-Data-Loc misses {NAT} by AMI_2:20, ZFMISC_1:50;
then A1: SCM-Data-Loc misses {NAT} ;
thus Data-Locations = ({NAT} \/ SCM-Data-Loc) \ {NAT} by AMI_2:22, SUBSET_1:def 8
.= (SCM-Data-Loc \/ {NAT}) \ {NAT}
.= SCM-Data-Loc \ {NAT} by XBOOLE_1:40
.= SCM-Data-Loc by A1, XBOOLE_1:83 ; :: thesis: verum