let X be set ; :: thesis: for F being BinOp of X ex A being Subset of X st
for x being set st x in [:A,A:] holds
F . x in A
let F be BinOp of X; :: thesis: ex A being Subset of X st
for x being set st x in [:A,A:] holds
F . x in A
X c= X ;
then reconsider Z = X as Subset of X ;
take Z ; :: thesis: for x being set st x in [:Z,Z:] holds
F . x in Z
thus for x being set st x in [:Z,Z:] holds
F . x in Z by Th1; :: thesis: verum