let R1, R2 be Relation; :: thesis: R1 \, R2 c= R1 \/ R2
let x, y be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in R1 \, R2 or [x,y] in R1 \/ R2 )
reconsider xx = x, yy = y as set by TARSKI:1;
assume [x,y] in R1 \, R2 ; :: thesis: [x,y] in R1 \/ R2
then xx,yy in R1 \, R2 ;
then ( xx,yy in R1 or xx,yy in R2 ) by Th9;
then ( [x,y] in R1 or [x,y] in R2 ) ;
hence [x,y] in R1 \/ R2 by XBOOLE_0:def 3; :: thesis: verum