let o1, o2 be BinOp of (Subgroups G); ( ( for H1, H2 being strict Subgroup of G holds o1 . (H1,H2) = H1 /\ H2 ) & ( for H1, H2 being strict Subgroup of G holds o2 . (H1,H2) = H1 /\ H2 ) implies o1 = o2 )
assume that
A3:
for H1, H2 being strict Subgroup of G holds o1 . (H1,H2) = H1 /\ H2
and
A4:
for H1, H2 being strict Subgroup of G holds o2 . (H1,H2) = H1 /\ H2
; o1 = o2
now for x, y being set st x in Subgroups G & y in Subgroups G holds
o1 . (x,y) = o2 . (x,y)let x,
y be
set ;
( x in Subgroups G & y in Subgroups G implies o1 . (x,y) = o2 . (x,y) )assume A5:
(
x in Subgroups G &
y in Subgroups G )
;
o1 . (x,y) = o2 . (x,y)then reconsider A =
x,
B =
y as
Element of
Subgroups G ;
reconsider H1 =
x,
H2 =
y as
strict Subgroup of
G by A5, GROUP_3:def 1;
o1 . (
A,
B)
= H1 /\ H2
by A3;
hence
o1 . (
x,
y)
= o2 . (
x,
y)
by A4;
verum end;
hence
o1 = o2
by BINOP_1:1; verum