reconsider F = {{}} as Subset-Family of P by SETFAM_1:46;
take F ; :: thesis: ( not F is empty & F is pcs-self-coherent-membered )
thus not F is empty ; :: thesis: F is pcs-self-coherent-membered
let S be Subset of P; :: according to PCS_0:def 45 :: thesis: ( S in F implies S is pcs-self-coherent )
assume S in F ; :: thesis: S is pcs-self-coherent
then S = {} P by TARSKI:def 1;
hence S is pcs-self-coherent ; :: thesis: verum