let X1 be non empty set ; :: thesis: {} X1 = { x1 where x1 is Element of X1 : contradiction }
thus {} X1 c= { x1 where x1 is Element of X1 : contradiction } :: according to XBOOLE_0:def 10 :: thesis: { x1 where x1 is Element of X1 : contradiction } c= {} X1

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in {} X1 or a in { x1 where x1 is Element of X1 : contradiction } )
thus ( not a in {} X1 or a in { x1 where x1 is Element of X1 : contradiction } ) ; :: thesis: verum

end;

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { x1 where x1 is Element of X1 : contradiction } or a in {} X1 )
assume a in { x1 where x1 is Element of X1 : contradiction } ; :: thesis: a in {} X1
then ex x1 being Element of X1 st
( a = x1 & contradiction ) ;
hence a in {} X1 ; :: thesis: verum