let S be Subset of P; :: thesis: ( S is empty implies S is pcs-self-coherent )
assume A1: S is empty ; :: thesis: S is pcs-self-coherent
let x be Element of P; :: according to PCS_0:def 43 :: thesis: for y being Element of P st x in S & y in S holds
x (--) y
thus for y being Element of P st x in S & y in S holds
x (--) y by A1; :: thesis: verum