let
x
,
y
,
z
be
Element
of 1;
:: thesis:
op2
.
(
x
,
z
)
<=
(
op2
.
(
x
,
y
)
)
+
(
op2
.
(
y
,
z
)
)
(
x
=
{}
&
y
=
{}
)
by
CARD_1:49
,
TARSKI:def 1
;
hence
op2
.
(
x
,
z
)
<=
(
op2
.
(
x
,
y
)
)
+
(
op2
.
(
y
,
z
)
)
by
Lm2
;
:: thesis:
verum