let A, B be Ordinal; :: thesis: for R being Relation st A c= B holds
ClosedProd (R,A,A) c= ClosedProd (R,B,B)
let R be Relation; :: thesis: ( A c= B implies ClosedProd (R,A,A) c= ClosedProd (R,B,B) )
assume A c= B ; :: thesis: ClosedProd (R,A,A) c= ClosedProd (R,B,B)
then ( A = B or A in B ) by ORDINAL1:11, XBOOLE_0:def 8;
hence ClosedProd (R,A,A) c= ClosedProd (R,B,B) by Th17; :: thesis: verum