defpred S₁[ Element of T, Element of T] means ex a being adjective of T st
( not a in adjs $2 & a is_properly_applicable_to $2 & a ast $2 = $1 );
consider R being Relation of the carrier of T such that
A1: for t1, t2 being Element of T holds
( [t1,t2] in R iff S₁[t1,t2] ) from RELSET_1:sch 2();
reconsider R = R as Relation of T ;
take R ; :: thesis: for t1, t2 being type of T holds
( [t1,t2] in R iff ex a being adjective of T st
( not a in adjs t2 & a is_properly_applicable_to t2 & a ast t2 = t1 ) )
thus for t1, t2 being type of T holds
( [t1,t2] in R iff ex a being adjective of T st
( not a in adjs t2 & a is_properly_applicable_to t2 & a ast t2 = t1 ) ) by A1; :: thesis: verum