let S be Subset of ; :: 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 ; :: according to PCS_0:def 43 :: thesis: for y being Element of st x in S & y in S holds
x (--) y
thus for y being Element of st x in S & y in S holds
x (--) y by A1; :: thesis: verum