let P, R be Relation; :: thesis: (P \/ R) ~ = (P ~ ) \/ (R ~ )
let x be set ; :: according to RELAT_1:def 2 :: thesis: for b being set holds
( [x,b] in (P \/ R) ~ iff [x,b] in (P ~ ) \/ (R ~ ) )
let y be set ; :: thesis: ( [x,y] in (P \/ R) ~ iff [x,y] in (P ~ ) \/ (R ~ ) )
( [x,y] in (P \/ R) ~ iff [y,x] in P \/ R ) by Def7;
then ( [x,y] in (P \/ R) ~ iff ( [y,x] in P or [y,x] in R ) ) by XBOOLE_0:def 3;
then ( [x,y] in (P \/ R) ~ iff ( [x,y] in P ~ or [x,y] in R ~ ) ) by Def7;
hence ( [x,y] in (P \/ R) ~ iff [x,y] in (P ~ ) \/ (R ~ ) ) by XBOOLE_0:def 3; :: thesis: verum