let E be set ; :: thesis: for A being Subset of (E ^omega ) holds A |^ 1,2 = A \/ (A ^^ A)
let A be Subset of (E ^omega ); :: thesis: A |^ 1,2 = A \/ (A ^^ A)
thus A |^ 1,2 = (A |^ 1) \/ (A |^ (1 + 1)) by Th28
.= A \/ (A |^ 2) by FLANG_1:26
.= A \/ (A ^^ A) by FLANG_1:27 ; :: thesis: verum