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: ex_inf_of X, InclPoset (Aux L)
set N = meet X;

per cases ( X <> {} or X = {} ) ;

suppose A1: X <> {} ; :: thesis: ex_inf_of X, InclPoset (Aux L)

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: ( X is_>=_than b implies N >= b )
assume A3: X is_>=_than b ; :: thesis: N >= b
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: verum

end;

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

end;

suppose X = {} ; :: thesis: ex_inf_of X, InclPoset (Aux L)

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

end;

end;

end;

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