let X be set ; :: thesis: for x, y being object

for R being Relation of X st R is_reflexive_in X & R reduces x,y & x in X holds

[x,y] in R [*]

let x, y be object ; :: thesis: for R being Relation of X st R is_reflexive_in X & R reduces x,y & x in X holds

[x,y] in R [*]

let R be Relation of X; :: thesis: ( R is_reflexive_in X & R reduces x,y & x in X implies [x,y] in R [*] )

assume A1: R is_reflexive_in X ; :: thesis: ( not R reduces x,y or not x in X or [x,y] in R [*] )

assume that

A2: R reduces x,y and

A3: x in X ; :: thesis: [x,y] in R [*]

for R being Relation of X st R is_reflexive_in X & R reduces x,y & x in X holds

[x,y] in R [*]

let x, y be object ; :: thesis: for R being Relation of X st R is_reflexive_in X & R reduces x,y & x in X holds

[x,y] in R [*]

let R be Relation of X; :: thesis: ( R is_reflexive_in X & R reduces x,y & x in X implies [x,y] in R [*] )

assume A1: R is_reflexive_in X ; :: thesis: ( not R reduces x,y or not x in X or [x,y] in R [*] )

assume that

A2: R reduces x,y and

A3: x in X ; :: thesis: [x,y] in R [*]