let L be non empty RelStr ; :: thesis: id L is monotone
let l1, l2 be Element of L; :: according to ORDERS_3:def 5 :: thesis: ( not l1 <= l2 or for b₁, b₂ being Element of the carrier of L holds
( not b₁ = (id L) . l1 or not b₂ = (id L) . l2 or b₁ <= b₂ ) )
assume l1 <= l2 ; :: thesis: for b₁, b₂ being Element of the carrier of L holds
( not b₁ = (id L) . l1 or not b₂ = (id L) . l2 or b₁ <= b₂ )
then l1 <= (id L) . l2 by FUNCT_1:18;
hence for b₁, b₂ being Element of the carrier of L holds
( not b₁ = (id L) . l1 or not b₂ = (id L) . l2 or b₁ <= b₂ ) by FUNCT_1:18; :: thesis: verum