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 Def9;
then reconsider N = meet X as Element of (InclPoset (Aux L)) by YELLOW_1:1;
A2: X is_>=_than N

proof

let b be Element of (InclPoset (Aux L)); :: according to LATTICE3:def 8 :: thesis: ( not b in X or N <= b )
assume b in X ; :: thesis: N <= b
then N c= b by SETFAM_1:4;
hence N <= b by YELLOW_1:3; :: thesis: verum

end;

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

proof

let Z1 be set ; :: thesis: ( Z1 in X implies b c= Z1 )
assume A4: Z1 in X ; :: thesis: b c= Z1
then reconsider Z19 = Z1 as Element of (InclPoset (Aux L)) ;
b <= Z19 by A3, A4, LATTICE3:def 8;
hence b c= Z1 by YELLOW_1:3; :: thesis: verum

end;

then b c= meet X by A1, SETFAM_1:6;
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:30; :: thesis: verum