let x be set ; :: thesis: ( x in PARTITIONS Y implies ex z being set st S₁[x,z] )
assume A2: x in PARTITIONS Y ; :: thesis: ex z being set st S₁[x,z]
reconsider x = x as a_partition of Y by A2, Def3;
take ERl x ; :: thesis: S₁[x, ERl x]
thus S₁[x, ERl x] ; :: thesis: verum