let T be non empty RelStr ; :: thesis: id T is monotone
set IT = id T;
let p1, p2 be Element of T; :: according to ORDERS_3:def 5 :: thesis: ( p1 <= p2 implies for a, b being Element of T st a = (id T) . p1 & b = (id T) . p2 holds
a <= b )
assume A1: p1 <= p2 ; :: thesis: for a, b being Element of T st a = (id T) . p1 & b = (id T) . p2 holds
a <= b
reconsider p1' = p1, p2' = p2 as Element of T ;
A2: ( (id T) . p1' = p1' & (id T) . p2' = p2' ) by TMAP_1:91;
let r1, r2 be Element of T; :: thesis: ( r1 = (id T) . p1 & r2 = (id T) . p2 implies r1 <= r2 )
assume ( r1 = (id T) . p1 & r2 = (id T) . p2 ) ; :: thesis: r1 <= r2
hence r1 <= r2 by A1, A2; :: thesis: verum