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) and
b in field (P /\ R) and
A2: [a,b] in P /\ R and
A3: [b,a] in P /\ R ; :: thesis: a = b
A4: [b,a] in P by A3, XBOOLE_0:def 4;
A5: [a,b] in P by A2, XBOOLE_0:def 4;
then ( a in field P & b in field P ) by RELAT_1:15;
hence a = b by A1, A5, A4, 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) and
b in field (P \ R) and
A6: [a,b] in P \ R and
A7: [b,a] in P \ R ; :: thesis: a = b
A8: [b,a] in P by A7, XBOOLE_0:def 5;
A9: [a,b] in P by A6, XBOOLE_0:def 5;
then ( a in field P & b in field P ) by RELAT_1:15;
hence a = b by A1, A9, A8, Def4; :: thesis: verum

end;

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