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

proof

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

end;

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