let E be set ; :: thesis: for A being Subset of (E ^omega ) holds (A + ) ^^ (A ? ) = (A ? ) ^^ (A + )
let A be Subset of (E ^omega ); :: thesis: (A + ) ^^ (A ? ) = (A ? ) ^^ (A + )
thus (A + ) ^^ (A ? ) = (A + ) ^^ (A |^ 0 ,1) by FLANG_2:79
.= (A |^ 0 ,1) ^^ (A + ) by Th72
.= (A ? ) ^^ (A + ) by FLANG_2:79 ; :: thesis: verum