let X be non empty finite set ; :: thesis:
let x be Element of X; :: thesis:
defpred S₁[ set ] means ex S being non empty Subset of X st
( $1 = meet S & ( for s being set st s in S holds
s is_/\-irreducible_in X ) );

A1: now :: thesis:

let x, y be set ; :: thesis:
assume that
x in X and
y in X and
A2: S₁[x] and
A3: S₁[y] ; :: thesis:
consider Sy being non empty Subset of X such that
A4: y = meet Sy and
A5: for s being set st s in Sy holds
s is_/\-irreducible_in X by A3;
consider Sx being non empty Subset of X such that
A6: x = meet Sx and
A7: for s being set st s in Sx holds
s is_/\-irreducible_in X by A2;
reconsider S = Sx \/ Sy as non empty Subset of X ;

now :: thesis:

take S = S; :: thesis:
thus x /\ y = meet S by A6, A4, SETFAM_1:9; :: thesis:
let s be set ; :: thesis:
assume A8: s in S ; :: thesis:

per cases by A8, XBOOLE_0:def 3;

suppose s in Sx ; :: thesis:

hence s is_/\-irreducible_in X by A7; :: thesis:

end;

suppose s in Sy ; :: thesis:

hence s is_/\-irreducible_in X by A5; :: thesis:

end;

end;

end;

hence S₁[x /\ y] ; :: thesis:

end;

A9: now :: thesis:

let x be set ; :: thesis:
assume A10: x is_/\-irreducible_in X ; :: thesis:
thus S₁[x] :: thesis:

proof

x in X by A10;
then reconsider S = {x} as non empty Subset of X by ZFMISC_1:31;
take S ; :: thesis:
thus x = meet S by SETFAM_1:10; :: thesis:
let s be set ; :: thesis:
assume s in S ; :: thesis:
hence s is_/\-irreducible_in X by A10, TARSKI:def 1; :: thesis:

end;

end;

for x being set st x in X holds
S₁[x] from ARMSTRNG:sch 2(A9, A1);
hence ex A being non empty Subset of X st
( x = meet A & ( for s being set st s in A holds
s is_/\-irreducible_in X ) ) ; :: thesis: