let R1, R2 be Relation of T; :: thesis: ( ( for t1, t2 being type of T holds
( [t1,t2] in R1 iff ex a being adjective of T st
( not a in adjs t2 & a is_properly_applicable_to t2 & a ast t2 = t1 ) ) ) & ( for t1, t2 being type of T holds
( [t1,t2] in R2 iff ex a being adjective of T st
( not a in adjs t2 & a is_properly_applicable_to t2 & a ast t2 = t1 ) ) ) implies R1 = R2 )
assume that
A2: for t1, t2 being type of T holds
( [t1,t2] in R1 iff ex a being adjective of T st
( not a in adjs t2 & a is_properly_applicable_to t2 & a ast t2 = t1 ) ) and
A3: for t1, t2 being type of T holds
( [t1,t2] in R2 iff ex a being adjective of T st
( not a in adjs t2 & a is_properly_applicable_to t2 & a ast t2 = t1 ) ) ; :: thesis: R1 = R2
let t1, t2 be Element of T; :: according to RELSET_1:def 2 :: thesis: ( ( not [t1,t2] in R1 or [t1,t2] in R2 ) & ( not [t1,t2] in R2 or [t1,t2] in R1 ) )
( [t1,t2] in R1 iff ex a being adjective of T st
( not a in adjs t2 & a is_properly_applicable_to t2 & a ast t2 = t1 ) ) by A2;
hence ( [t1,t2] in R1 iff [t1,t2] in R2 ) by A3; :: thesis: verum