let P, R be Relation; :: thesis: ( P is antisymmetric implies ( P /\ R is antisymmetric & P \ R is antisymmetric ) )
assume P is antisymmetric ; :: thesis: ( P /\ R is antisymmetric & P \ R is antisymmetric )
then A1: P is_antisymmetric_in field P by Def12;

now

let a, b be set ; :: thesis: ( a in field (P /\ R) & b in field (P /\ R) & [a,b] in P /\ R & [b,a] in P /\ R implies a = b )
assume that
( a in field (P /\ R) & b in field (P /\ R) ) and
A2: ( [a,b] in P /\ R & [b,a] in P /\ R ) ; :: thesis: a = b
A3: ( [a,b] in P & [b,a] in P ) by A2, XBOOLE_0:def 4;
then ( a in field P & b in field P ) by RELAT_1:30;
hence a = b by A1, A3, Def4; :: thesis: verum

end;

then P /\ R is_antisymmetric_in field (P /\ R) by Def4;
hence P /\ R is antisymmetric by Def12; :: thesis: P \ R is antisymmetric

now

let a, b be set ; :: thesis: ( a in field (P \ R) & b in field (P \ R) & [a,b] in P \ R & [b,a] in P \ R implies a = b )
assume that
( a in field (P \ R) & b in field (P \ R) ) and
A4: ( [a,b] in P \ R & [b,a] in P \ R ) ; :: thesis: a = b
A5: ( [a,b] in P & not [a,b] in R & [b,a] in P & not [b,a] in R ) by A4, XBOOLE_0:def 5;
then ( a in field P & b in field P ) by RELAT_1:30;
hence a = b by A1, A5, Def4; :: thesis: verum

end;

then P \ R is_antisymmetric_in field (P \ R) by Def4;
hence P \ R is antisymmetric by Def12; :: thesis: verum