consider x, y being Element of T such that
A1: x <> y by STRUCT_0:def 10;
take X = {x,y}; :: thesis: not X is trivial
A2: y in X by TARSKI:def 2;
x in X by TARSKI:def 2;
hence not X is trivial by A1, A2, REALSET1:15; :: thesis: verum