let L be lower-bounded with_suprema Poset; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: [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; :: thesis: verum

end;

hence a /\ b is auxiliary(ii) Relation of L by Def4; :: thesis: verum