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
let r1, r2 be Element of T; :: thesis: ( r1 = (id T) . p1 & r2 = (id T) . p2 implies r1 <= r2 )
reconsider p19 = p1, p29 = p2 as Element of T ;
A2: (id T) . p19 = p19 by FUNCT_1:35;
assume ( r1 = (id T) . p1 & r2 = (id T) . p2 ) ; :: thesis: r1 <= r2
hence r1 <= r2 by A1, A2, FUNCT_1:35; :: thesis: verum