defpred S1[ Element of Union (G,RK), Element of Union (G,RK), set ] means for x, y being Element of X st $1 = x & $2 = y holds
$3 = x \ y;
A1:
for w1, w2 being Element of Union (G,RK) ex v being Element of Union (G,RK) st S1[w1,w2,v]
proof
let w1,
w2 be
Element of
Union (
G,
RK);
ex v being Element of Union (G,RK) st S1[w1,w2,v]
consider a being
Element of
G such that A2:
w1 in Class (
RK,
a)
by Lm5;
A3:
[a,w1] in RK
by A2, EQREL_1:18;
consider b being
Element of
G such that A4:
w2 in Class (
RK,
b)
by Lm5;
the
carrier of
G c= the
carrier of
X
by BCIALG_1:def 10;
then reconsider a1 =
a,
b1 =
b as
Element of
X ;
Class (
RK,
(a1 \ b1))
in the
carrier of
(X ./. RK)
by EQREL_1:def 3;
then
Class (
RK,
(a \ b))
in the
carrier of
(X ./. RK)
by Th34;
then A5:
Class (
RK,
(a \ b))
in { (Class (RK,c)) where c is Element of G : Class (RK,c) in the carrier of (X ./. RK) }
;
A6:
[b,w2] in RK
by A4, EQREL_1:18;
reconsider w1 =
w1,
w2 =
w2 as
Element of
X ;
[(a1 \ b1),(w1 \ w2)] in RK
by A3, A6, BCIALG_2:def 9;
then
w1 \ w2 in Class (
RK,
(a1 \ b1))
by EQREL_1:18;
then
w1 \ w2 in Class (
RK,
(a \ b))
by Th34;
then reconsider C =
w1 \ w2 as
Element of
Union (
G,
RK)
by A5, TARSKI:def 4;
take
C
;
S1[w1,w2,C]
thus
S1[
w1,
w2,
C]
;
verum
end;
thus
ex B being BinOp of (Union (G,RK)) st
for w1, w2 being Element of Union (G,RK) holds S1[w1,w2,B . (w1,w2)]
from BINOP_1:sch 3(A1); verum