let X be set ; :: thesis: {} c= X
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {} or x in X )
thus ( not x in {} or x in X ) ; :: thesis: verum