let F be net_set of X,T; :: thesis: F is RelStr-yielding
let v be set ; :: according to YELLOW_1:def 3 :: thesis: ( not v in proj2 F or v is RelStr )
assume v in rng F ; :: thesis: v is RelStr
hence v is RelStr by Def12; :: thesis: verum