let a be object ; :: thesis: for X being set
for R being Relation holds (R |_2 X) -Seg a c= R -Seg a
let X be set ; :: thesis: for R being Relation holds (R |_2 X) -Seg a c= R -Seg a
let R be Relation; :: thesis: (R |_2 X) -Seg a c= R -Seg a
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (R |_2 X) -Seg a or x in R -Seg a )
assume A1: x in (R |_2 X) -Seg a ; :: thesis: x in R -Seg a
then [x,a] in R |_2 X by Th1;
then A2: [x,a] in R by XBOOLE_0:def 4;
x <> a by A1, Th1;
hence x in R -Seg a by A2, Th1; :: thesis: verum