let X, Y be set ; :: thesis: for P being Relation st P is_reflexive_in X & Y c= X holds
P is_reflexive_in Y
let P be Relation; :: thesis: ( P is_reflexive_in X & Y c= X implies P is_reflexive_in Y )
assume that
A1: P is_reflexive_in X and
A2: Y c= X ; :: thesis: P is_reflexive_in Y
let x be set ; :: according to RELAT_2:def 1 :: thesis: ( not x in Y or [x,x] in P )
assume x in Y ; :: thesis: [x,x] in P
hence [x,x] in P by A1, A2, RELAT_2:def 1; :: thesis: verum