let E be set ; :: thesis: for A being Subset of (E ^omega ) holds A |^ 0 ,2 = ({(<%> E)} \/ A) \/ (A ^^ A)
let A be Subset of (E ^omega ); :: thesis: A |^ 0 ,2 = ({(<%> E)} \/ A) \/ (A ^^ A)
thus A |^ 0 ,2 = (A |^ 0 ,1) \/ (A |^ (1 + 1)) by Th26
.= ({(<%> E)} \/ A) \/ (A |^ (1 + 1)) by Th46
.= ({(<%> E)} \/ A) \/ (A ^^ A) by FLANG_1:27 ; :: thesis: verum