take Stop S ; :: thesis: not Stop S is program-free
dom (Stop S) = {0} by FUNCOP_1:19;
then dom (Stop S) c= NAT ;
then (Stop S) | NAT = Stop S by RELAT_1:97;
hence (Stop S) | NAT <> {} ; :: according to COMPOS_1:def 29 :: thesis: verum