let E be set ; for A, B being Subset of (E ^omega) st <%> E in A & <%> E in B holds
( A ? c= A ^^ B & A ? c= B ^^ A )
let A, B be Subset of (E ^omega); ( <%> E in A & <%> E in B implies ( A ? c= A ^^ B & A ? c= B ^^ A ) )
assume that
A1:
<%> E in A
and
A2:
<%> E in B
; ( A ? c= A ^^ B & A ? c= B ^^ A )
<%> E in B ^^ A
by A1, A2, FLANG_1:15;
then A3:
{(<%> E)} c= B ^^ A
by ZFMISC_1:31;
<%> E in A ^^ B
by A1, A2, FLANG_1:15;
then A4:
{(<%> E)} c= A ^^ B
by ZFMISC_1:31;
A c= B ^^ A
by A2, FLANG_1:16;
then A5:
{(<%> E)} \/ A c= B ^^ A
by A3, XBOOLE_1:8;
A c= A ^^ B
by A2, FLANG_1:16;
then
{(<%> E)} \/ A c= A ^^ B
by A4, XBOOLE_1:8;
hence
( A ? c= A ^^ B & A ? c= B ^^ A )
by A5, Th76; verum