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

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