let Y be set ; :: thesis: for U being non empty set
for x, y being Element of U holds
not ( ( x in Y implies y in Y ) & ( y in Y implies x in Y ) & not [((chi (Y,U)) . x),((chi (Y,U)) . y)] in id BOOLEAN )
let U be non empty set ; :: thesis: for x, y being Element of U holds
not ( ( x in Y implies y in Y ) & ( y in Y implies x in Y ) & not [((chi (Y,U)) . x),((chi (Y,U)) . y)] in id BOOLEAN )
let x, y be Element of U; :: thesis: not ( ( x in Y implies y in Y ) & ( y in Y implies x in Y ) & not [((chi (Y,U)) . x),((chi (Y,U)) . y)] in id BOOLEAN )
set f = chi (Y,U);
assume A1: ( x in Y iff y in Y ) ; :: thesis: [((chi (Y,U)) . x),((chi (Y,U)) . y)] in id BOOLEAN
per cases ( x in Y or not x in Y ) ;
suppose x in Y ; :: thesis: [((chi (Y,U)) . x),((chi (Y,U)) . y)] in id BOOLEAN
then ( (chi (Y,U)) . x = 1 & y in Y ) by A1, RFUNCT_1:63;
then ( (chi (Y,U)) . x = 1 & (chi (Y,U)) . y = 1 & 1 in BOOLEAN ) by RFUNCT_1:63;
hence [((chi (Y,U)) . x),((chi (Y,U)) . y)] in id BOOLEAN by RELAT_1:def 10; :: thesis: verum
end;
suppose not x in Y ; :: thesis: [((chi (Y,U)) . x),((chi (Y,U)) . y)] in id BOOLEAN
then ( (chi (Y,U)) . x = 0 & not y in Y ) by A1, RFUNCT_1:64;
then ( (chi (Y,U)) . x = 0 & (chi (Y,U)) . y = 0 & 0 in BOOLEAN ) by RFUNCT_1:64;
hence [((chi (Y,U)) . x),((chi (Y,U)) . y)] in id BOOLEAN by RELAT_1:def 10; :: thesis: verum
end;
end;