let L be lower-bounded with_suprema Poset; :: thesis: for X being non empty Subset of (InclPoset (Aux L)) holds meet X is auxiliary Relation of L
let X be non empty Subset of (InclPoset (Aux L)); :: thesis: meet X is auxiliary Relation of L
X c= the carrier of (InclPoset (Aux L)) ;
then A1: X c= Aux L by YELLOW_1:1;
consider a being Element of X;
a in X ;
then a is auxiliary Relation of L by A1, Def9;
then meet X c= [:the carrier of L,the carrier of L:] by SETFAM_1:8;
then reconsider ab = meet X as Relation of L ;

now

thus ab is auxiliary(i) :: thesis: ( ab is auxiliary(ii) & ab is auxiliary(iii) & ab is auxiliary(iv) )

proof

let x, y be Element of L; :: according to WAYBEL_4:def 4 :: thesis: ( [x,y] in ab implies x <= y )
assume A2: [x,y] in ab ; :: thesis: x <= y
consider V being Element of X;
A3: V in X ;
A4: [x,y] in V by A2, SETFAM_1:def 1;
V is auxiliary Relation of L by A1, A3, Def9;
hence x <= y by A4, Def4; :: thesis: verum

end;

thus ab is auxiliary(ii) :: thesis: ( ab is auxiliary(iii) & ab is auxiliary(iv) )

proof

let x, y, z, u be Element of L; :: according to WAYBEL_4:def 5 :: thesis: ( u <= x & [x,y] in ab & y <= z implies [u,z] in ab )
assume A5: ( u <= x & [x,y] in ab & y <= z ) ; :: thesis: [u,z] in ab
for Y being set st Y in X holds
[u,z] in Y

proof

let Y be set ; :: thesis: ( Y in X implies [u,z] in Y )
assume A6: Y in X ; :: thesis: [u,z] in Y
then A7: Y is auxiliary Relation of L by A1, Def9;
[x,y] in Y by A5, A6, SETFAM_1:def 1;
hence [u,z] in Y by A5, A7, Def5; :: thesis: verum

end;

hence [u,z] in ab by SETFAM_1:def 1; :: thesis: verum

end;

thus ab is auxiliary(iii) :: thesis: ab is auxiliary(iv)

proof

let x, y, z be Element of L; :: according to WAYBEL_4:def 6 :: thesis: ( [x,z] in ab & [y,z] in ab implies [(x "\/" y),z] in ab )
assume A8: ( [x,z] in ab & [y,z] in ab ) ; :: thesis: [(x "\/" y),z] in ab
for Y being set st Y in X holds
[(x "\/" y),z] in Y

proof

let Y be set ; :: thesis: ( Y in X implies [(x "\/" y),z] in Y )
assume A9: Y in X ; :: thesis: [(x "\/" y),z] in Y
then A10: Y is auxiliary Relation of L by A1, Def9;
( [x,z] in Y & [y,z] in Y ) by A8, A9, SETFAM_1:def 1;
hence [(x "\/" y),z] in Y by A10, Def6; :: thesis: verum

end;

hence [(x "\/" y),z] in ab by SETFAM_1:def 1; :: thesis: verum

end;

thus ab is auxiliary(iv) :: thesis: verum

proof

let x be Element of L; :: according to WAYBEL_4:def 7 :: thesis: [(Bottom L),x] in ab
for Y being set st Y in X holds
[(Bottom L),x] in Y

proof

let Y be set ; :: thesis: ( Y in X implies [(Bottom L),x] in Y )
assume Y in X ; :: thesis: [(Bottom L),x] in Y
then Y is auxiliary Relation of L by A1, Def9;
hence [(Bottom L),x] in Y by Def7; :: thesis: verum

end;

hence [(Bottom L),x] in ab by SETFAM_1:def 1; :: thesis: verum

end;

end;

hence meet X is auxiliary Relation of L ; :: thesis: verum