let E be set ; :: thesis: for A, B being Subset of (E ^omega ) holds (A /\ B) ? = (A ? ) /\ (B ? )
let A, B be Subset of (E ^omega ); :: thesis: (A /\ B) ? = (A ? ) /\ (B ? )
thus (A /\ B) ? = {(<%> E)} \/ (A /\ B) by Th76
.= ({(<%> E)} \/ A) /\ ({(<%> E)} \/ B) by XBOOLE_1:24
.= (A ? ) /\ ({(<%> E)} \/ B) by Th76
.= (A ? ) /\ (B ? ) by Th76 ; :: thesis: verum