let T be non empty RelStr ; :: thesis: for A, B being Subset of T holds (A ^d) /\ (B ^d) = (A /\ B) ^d
let A, B be Subset of T; :: thesis: (A ^d) /\ (B ^d) = (A /\ B) ^d
A1: B ^d = ((B `) ^f) ` by Th4;
thus (A ^d) /\ (B ^d) = (((A `) ^f) `) /\ (B ^d) by Th4
.= (((A `) ^f) \/ ((B `) ^f)) ` by A1, XBOOLE_1:53
.= (((A `) \/ (B `)) ^f) ` by Th11
.= (((A /\ B) `) ^f) ` by XBOOLE_1:54
.= (A /\ B) ^d by Th4 ; :: thesis: verum