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