let X be set ; :: thesis: for A being Subset of X holds A is pr1 (X,X) -binopclosed
let A be Subset of X; :: thesis: A is pr1 (X,X) -binopclosed
set S = pr1 (X,X);
for x being set st x in [:A,A:] holds
(pr1 (X,X)) . x in A
proof
let x be set ; :: thesis: ( x in [:A,A:] implies (pr1 (X,X)) . x in A )
assume x in [:A,A:] ; :: thesis: (pr1 (X,X)) . x in A
then consider p, q being object such that
A1: ( p in A & q in A ) and
A2: x = [p,q] by ZFMISC_1:def 2;
(pr1 (X,X)) . x = (pr1 (X,X)) . (p,q) by A2;
hence (pr1 (X,X)) . x in A by A1, FUNCT_3:def 4; :: thesis: verum
end;
hence A is pr1 (X,X) -binopclosed ; :: thesis: verum