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 A1: ( u <= x & [x,y] in ab & y <= z ) ; :: thesis: [u,z] in ab
then ( [x,y] in a & [x,y] in b ) by XBOOLE_0:def 4;
then ( [u,z] in a & [u,z] in b ) by A1, Def5;
hence [u,z] in ab by XBOOLE_0:def 4; :: thesis: verum

end;

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