let X be set ; for A being Subset of X holds A is pr1 (X,X) -binopclosed
let A be Subset of X; 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 ;
( x in [:A,A:] implies (pr1 (X,X)) . x in A )
assume
x in [:A,A:]
;
(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;
verum
end;
hence
A is pr1 (X,X) -binopclosed
; verum