let X be non empty finite set ; :: thesis: for x being Element of X 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 ) )
let x be Element of X; :: thesis: 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 ) )
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

let x be set ; :: thesis: ( x is_/\-irreducible_in X implies S₁[x] )
assume A2: x is_/\-irreducible_in X ; :: thesis: S₁[x]
thus S₁[x] :: thesis: verum

proof

x in X by A2, Def2;
then reconsider S = {x} as non empty Subset of X by ZFMISC_1:37;
take S ; :: thesis: ( x = meet S & ( for s being set st s in S holds
s is_/\-irreducible_in X ) )
thus x = meet S by SETFAM_1:11; :: thesis: for s being set st s in S holds
s is_/\-irreducible_in X
let s be set ; :: thesis: ( s in S implies s is_/\-irreducible_in X )
assume s in S ; :: thesis: s is_/\-irreducible_in X
hence s is_/\-irreducible_in X by A2, TARSKI:def 1; :: thesis: verum

end;

end;

A3: now

let x, y be set ; :: thesis: ( x in X & y in X & S₁[x] & S₁[y] implies S₁[x /\ y] )
assume that
( x in X & y in X ) and
A4: S₁[x] and
A5: S₁[y] ; :: thesis: S₁[x /\ y]
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 A4;
consider Sy being non empty Subset of X such that
A8: y = meet Sy and
A9: for s being set st s in Sy holds
s is_/\-irreducible_in X by A5;
reconsider S = Sx \/ Sy as non empty Subset of X ;

now

take S = S; :: thesis: ( x /\ y = meet S & ( for s being set st s in S holds
b₃ is_/\-irreducible_in X ) )
thus x /\ y = meet S by A6, A8, SETFAM_1:10; :: thesis: for s being set st s in S holds
b₃ is_/\-irreducible_in X
let s be set ; :: thesis: ( s in S implies b₂ is_/\-irreducible_in X )
assume A10: s in S ; :: thesis: b₂ is_/\-irreducible_in X

per cases ( s in Sx or s in Sy ) by A10, XBOOLE_0:def 3;

suppose s in Sx ; :: thesis: b₂ is_/\-irreducible_in X

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

end;

suppose s in Sy ; :: thesis: b₂ is_/\-irreducible_in X

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

end;

end;

end;

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

end;

for x being set st x in X holds
S₁[x] from ARMSTRNG:sch 2(A1, A3);
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: verum