let L be lower-bounded with_suprema Poset; for a, b being auxiliary(ii) Relation of L holds a /\ b is auxiliary(ii) Relation of L
let a, b be auxiliary(ii) Relation of L; a /\ b is auxiliary(ii) Relation of L
reconsider ab = a /\ b as Relation of L ;
for x, y, z, u being Element of L st u <= x & [x,y] in ab & y <= z holds
[u,z] in ab
proof
let x,
y,
z,
u be
Element of
L;
( u <= x & [x,y] in ab & y <= z implies [u,z] in ab )
assume that A1:
u <= x
and A2:
[x,y] in ab
and A3:
y <= z
;
[u,z] in ab
A4:
[x,y] in a
by A2, XBOOLE_0:def 4;
A5:
[x,y] in b
by A2, XBOOLE_0:def 4;
A6:
[u,z] in a
by A1, A3, A4, Def4;
[u,z] in b
by A1, A3, A5, Def4;
hence
[u,z] in ab
by A6, XBOOLE_0:def 4;
verum
end;
hence
a /\ b is auxiliary(ii) Relation of L
by Def4; verum