let Y be set ; :: thesis: for R being Relation holds Y | (Y | R) = Y | R
let R be Relation; :: thesis: Y | (Y | R) = Y | R
Y /\ Y = Y ;
hence Y | (Y | R) = Y | R by Th127; :: thesis: verum