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