let L be non empty RelStr ; :: thesis: id L is idempotent
thus (id L) * (id L) = id ( the carrier of L /\ the carrier of L) by FUNCT_1:22
.= id L ; :: according to QUANTAL1:def 9 :: thesis: verum