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
( x in X & y in X ) by TARSKI:def 2;
hence not X is trivial by A1, REALSET1:15; :: thesis: verum