let x, y be set ; :: thesis: for R, S being RelStr st [x,y] in the InternalRel of (R [*] S) & the carrier of R /\ the carrier of S is upper Subset of R & not ( x in the carrier of R & y in the carrier of R ) & not ( x in the carrier of S & y in the carrier of S ) holds
( x in the carrier of R \ the carrier of S & y in the carrier of S \ the carrier of R )
let R, S be RelStr ; :: thesis: ( [x,y] in the InternalRel of (R [*] S) & the carrier of R /\ the carrier of S is upper Subset of R & not ( x in the carrier of R & y in the carrier of R ) & not ( x in the carrier of S & y in the carrier of S ) implies ( x in the carrier of R \ the carrier of S & y in the carrier of S \ the carrier of R ) )
assume A1: ( [x,y] in the InternalRel of (R [*] S) & the carrier of R /\ the carrier of S is upper Subset of R ) ; :: thesis: ( ( x in the carrier of R & y in the carrier of R ) or ( x in the carrier of S & y in the carrier of S ) or ( x in the carrier of R \ the carrier of S & y in the carrier of S \ the carrier of R ) )
then ( x in the carrier of (R [*] S) & y in the carrier of (R [*] S) ) by ZFMISC_1:106;
then A2: ( x in the carrier of R \/ the carrier of S & y in the carrier of R \/ the carrier of S ) by Def2;

per cases ( ( x in the carrier of R & y in the carrier of R ) or ( x in the carrier of S & y in the carrier of S ) or ( x in the carrier of R & y in the carrier of S ) or ( x in the carrier of S & y in the carrier of R ) ) by A2, XBOOLE_0:def 3;

suppose ( x in the carrier of R & y in the carrier of R ) ; :: thesis: ( ( x in the carrier of R & y in the carrier of R ) or ( x in the carrier of S & y in the carrier of S ) or ( x in the carrier of R \ the carrier of S & y in the carrier of S \ the carrier of R ) )

hence ( ( x in the carrier of R & y in the carrier of R ) or ( x in the carrier of S & y in the carrier of S ) or ( x in the carrier of R \ the carrier of S & y in the carrier of S \ the carrier of R ) ) ; :: thesis: verum

end;

suppose ( x in the carrier of S & y in the carrier of S ) ; :: thesis: ( ( x in the carrier of R & y in the carrier of R ) or ( x in the carrier of S & y in the carrier of S ) or ( x in the carrier of R \ the carrier of S & y in the carrier of S \ the carrier of R ) )

hence ( ( x in the carrier of R & y in the carrier of R ) or ( x in the carrier of S & y in the carrier of S ) or ( x in the carrier of R \ the carrier of S & y in the carrier of S \ the carrier of R ) ) ; :: thesis: verum

end;

suppose ( x in the carrier of R & y in the carrier of S ) ; :: thesis: ( ( x in the carrier of R & y in the carrier of R ) or ( x in the carrier of S & y in the carrier of S ) or ( x in the carrier of R \ the carrier of S & y in the carrier of S \ the carrier of R ) )

hence ( ( x in the carrier of R & y in the carrier of R ) or ( x in the carrier of S & y in the carrier of S ) or ( x in the carrier of R \ the carrier of S & y in the carrier of S \ the carrier of R ) ) by XBOOLE_0:def 5; :: thesis: verum

end;

suppose ( x in the carrier of S & y in the carrier of R ) ; :: thesis: ( ( x in the carrier of R & y in the carrier of R ) or ( x in the carrier of S & y in the carrier of S ) or ( x in the carrier of R \ the carrier of S & y in the carrier of S \ the carrier of R ) )

hence ( ( x in the carrier of R & y in the carrier of R ) or ( x in the carrier of S & y in the carrier of S ) or ( x in the carrier of R \ the carrier of S & y in the carrier of S \ the carrier of R ) ) by A1, Th17; :: thesis: verum

end;

end;