set X = { ((NIC (i,l)) \ (JUMP i)) where i is Element of the InstructionsF of S : verum } ;
{ ((NIC (i,l)) \ (JUMP i)) where i is Element of the InstructionsF of S : verum } c= bool NAT

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { ((NIC (i,l)) \ (JUMP i)) where i is Element of the InstructionsF of S : verum } or x in bool NAT )
assume x in { ((NIC (i,l)) \ (JUMP i)) where i is Element of the InstructionsF of S : verum } ; :: thesis: x in bool NAT
then ex i being Element of the InstructionsF of S st x = (NIC (i,l)) \ (JUMP i) ;
hence x in bool NAT ; :: thesis: verum

end;

then reconsider X = { ((NIC (i,l)) \ (JUMP i)) where i is Element of the InstructionsF of S : verum } as Subset-Family of NAT ;
union X c= NAT ;
hence union { ((NIC (i,l)) \ (JUMP i)) where i is Element of the InstructionsF of S : verum } is Subset of NAT ; :: thesis: verum