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 that
A1: [x,y] in the InternalRel of (R [*] S) and
A2: 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 ) )
x in the carrier of (R [*] S) by A1, ZFMISC_1:87;
then A3: x in the carrier of R \/ the carrier of S by Def2;
y in the carrier of (R [*] S) by A1, ZFMISC_1:87;
then A4: 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 A3, A4, 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, A2, Th17; :: thesis: verum

end;

end;