let x be trivial set ; for y being Subset of x st not y is empty holds
x = y
let y be Subset of x; ( not y is empty implies x = y )
assume A1:
not y is empty
; x = y
then consider a being Element of x such that
A3:
x = {a}
by SUBSET_1:46;
consider b being Element of x such that
A4:
y = {b}
by A1, SUBSET_1:47;
thus
x = y
by A3, A4, SUBSET_1:def 7; verum