for X being Subset of (InclPoset (Aux L)) holds ex_inf_of X, InclPoset (Aux L)

proof

let X be Subset of (InclPoset (Aux L)); :: thesis:
set N = meet X;

per cases ;

suppose A1: X <> {} ; :: thesis:

then meet X is auxiliary Relation of L by Th11;
then meet X in Aux L by Def8;
then reconsider N = meet X as Element of (InclPoset (Aux L)) by YELLOW_1:1;
A2: X is_>=_than N by SETFAM_1:3, YELLOW_1:3;
for b being Element of (InclPoset (Aux L)) st X is_>=_than b holds
N >= b

proof

let b be Element of (InclPoset (Aux L)); :: thesis:
assume A3: X is_>=_than b ; :: thesis:
for Z1 being set st Z1 in X holds
b c= Z1 by A3, YELLOW_1:3;
then b c= meet X by A1, SETFAM_1:5;
hence N >= b by YELLOW_1:3; :: thesis:

end;

hence ex_inf_of X, InclPoset (Aux L) by A2, YELLOW_0:16; :: thesis:

end;

suppose X = {} ; :: thesis:

hence ex_inf_of X, InclPoset (Aux L) by YELLOW_0:43; :: thesis:

end;

end;

end;

hence InclPoset (Aux L) is complete by YELLOW_2:28; :: thesis: