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