let x, y be object ; :: thesis: Ext ({},x,y) = {}
assume Ext ({},x,y) <> {} ; :: thesis: contradiction
then consider a being object such that
A1: a in Ext ({},x,y) by XBOOLE_0:def 1;

per cases ( a in { (A \/ {y}) where A is Element of {} : x in A } or a in { A where A is Element of {} : ( not x in A & A in {} ) } ) by A1, XBOOLE_0:def 3;

suppose a in { (A \/ {y}) where A is Element of {} : x in A } ; :: thesis: contradiction

then ex A being Element of {} st
( a = A \/ {y} & x in A ) ;
hence contradiction by SUBSET_1:def 1; :: thesis: verum

end;

suppose a in { A where A is Element of {} : ( not x in A & A in {} ) } ; :: thesis: contradiction

then ex A being Element of {} st
( a = A & not x in A & A in {} ) ;
hence contradiction ; :: thesis: verum

end;

end;