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:26;
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 by TARSKI:def 3;
Class RK,
(a1 \ b1) in the
carrier of
(X ./. RK)
by EQREL_1:def 5;
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:26;
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:26;
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