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 [*]
per cases ( [x,y] in R [*] or x = y ) by A2, REWRITE1:20;
suppose [x,y] in R [*] ; :: thesis: [x,y] in R [*]
hence [x,y] in R [*] ; :: thesis: verum
end;
suppose A4: x = y ; :: thesis: [x,y] in R [*]
R [*] is_reflexive_in X by A1, Th5;
hence [x,y] in R [*] by A3, A4, RELAT_2:def 1; :: thesis: verum
end;
end;