let E be set ; :: thesis: for A, B being Subset of (E ^omega) holds
( A ^^ B = {(<%> E)} iff ( A = {(<%> E)} & B = {(<%> E)} ) )
let A, B be Subset of (E ^omega); :: thesis: ( A ^^ B = {(<%> E)} iff ( A = {(<%> E)} & B = {(<%> E)} ) )
thus ( A ^^ B = {(<%> E)} implies ( A = {(<%> E)} & B = {(<%> E)} ) ) :: thesis: ( A = {(<%> E)} & B = {(<%> E)} implies A ^^ B = {(<%> E)} )
proof
assume that
A1: A ^^ B = {(<%> E)} and
A2: ( A <> {(<%> E)} or B <> {(<%> E)} ) ; :: thesis: contradiction
<%> E in A ^^ B by A1, TARSKI:def 1;
then consider a, b being Element of E ^omega such that
A3: a in A and
A4: b in B and
<%> E = a ^ b by Def1;
A5: now :: thesis: for x being set st ( x in A or x in B ) holds
not x <> <%> E
let x be set ; :: thesis: ( ( x in A or x in B ) implies not x <> <%> E )
assume that
A6: ( x in A or x in B ) and
A7: x <> <%> E ; :: thesis: contradiction
A8: now :: thesis: not x in B
assume A9: x in B ; :: thesis: contradiction
then reconsider xb = x as Element of E ^omega ;
A10: a ^ xb <> <%> E by A7, AFINSQ_1:30;
a ^ xb in A ^^ B by A3, A9, Def1;
hence contradiction by A1, A10, TARSKI:def 1; :: thesis: verum
end;
now :: thesis: not x in A
assume A11: x in A ; :: thesis: contradiction
then reconsider xa = x as Element of E ^omega ;
A12: xa ^ b <> <%> E by A7, AFINSQ_1:30;
xa ^ b in A ^^ B by A4, A11, Def1;
hence contradiction by A1, A12, TARSKI:def 1; :: thesis: verum
end;
hence contradiction by A6, A8; :: thesis: verum
end;
then A13: for x being object holds
( x in B iff x = <%> E ) by A4;
for x being object holds
( x in A iff x = <%> E ) by A3, A5;
hence contradiction by A2, A13, TARSKI:def 1; :: thesis: verum
end;
assume ( A = {(<%> E)} & B = {(<%> E)} ) ; :: thesis: A ^^ B = {(<%> E)}
hence A ^^ B = {(<%> E)} by Th13; :: thesis: verum