let x be object ; :: thesis: ( x in PARTITIONS Y implies ex z being object st S_{1}[x,z] )

assume x in PARTITIONS Y ; :: thesis: ex z being object st S_{1}[x,z]

then reconsider x = x as a_partition of Y by Def3;

take ERl x ; :: thesis: S_{1}[x, ERl x]

thus S_{1}[x, ERl x]
; :: thesis: verum

assume x in PARTITIONS Y ; :: thesis: ex z being object st S

then reconsider x = x as a_partition of Y by Def3;

take ERl x ; :: thesis: S

thus S