Description: Membership in an initial segment. The idiom (`' A " { B } ) ,
meaning { x | x A B } ` , is used to specify an initial segment in
(for example) Definition 6.21 of TakeutiZaring p. 30. (Contributed by NM, 28-Apr-2004)(Proof shortened by Andrew Salmon, 27-Aug-2011)