take {} ; :: thesis: {} is non-empty
let x be object ; :: according to FUNCT_1:def 9 :: thesis: ( x in dom {} implies not {} . x is empty )
thus ( x in dom {} implies not {} . x is empty ) ; :: thesis: verum