let x be set ; :: thesis: for X being trivial set st x in X holds
X = {x}
let X be trivial set ; :: thesis: ( x in X implies X = {x} )
assume A1: x in X ; :: thesis: X = {x}
then ex x being object st X = {x} by Th130;
hence X = {x} by A1, TARSKI:def 1; :: thesis: verum