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