{ x where x is transition of CPNT1 : x is outbound } c= the carrier' of CPNT1

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { x where x is transition of CPNT1 : x is outbound } or z in the carrier' of CPNT1 )
assume z in { x where x is transition of CPNT1 : x is outbound } ; :: thesis: z in the carrier' of CPNT1
then ex x being transition of CPNT1 st
( z = x & x is outbound ) ;
hence z in the carrier' of CPNT1 ; :: thesis: verum

end;

hence { x where x is transition of CPNT1 : x is outbound } is Subset of the carrier' of CPNT1 ; :: thesis: verum