let X be set ; :: thesis: for S being with_empty_element cap-closed semi-diff-closed Subset-Family of X ex Y being non empty preBoolean Subset-Family of X st Y = meet { Z where Z is non empty preBoolean Subset-Family of X : S c= Z }
let S be with_empty_element cap-closed semi-diff-closed Subset-Family of X; :: thesis: ex Y being non empty preBoolean Subset-Family of X st Y = meet { Z where Z is non empty preBoolean Subset-Family of X : S c= Z }
set V = { Z where Z is non empty preBoolean Subset-Family of X : S c= Z } ;
A1: bool X in { Z where Z is non empty preBoolean Subset-Family of X : S c= Z } ;
then reconsider Y = meet { Z where Z is non empty preBoolean Subset-Family of X : S c= Z } as Subset-Family of X by SETFAM_1:3;

now :: thesis: for Z being set st Z in { Z where Z is non empty preBoolean Subset-Family of X : S c= Z } holds
{} in Z

let Z be set ; :: thesis: ( Z in { Z where Z is non empty preBoolean Subset-Family of X : S c= Z } implies {} in Z )
assume Z in { Z where Z is non empty preBoolean Subset-Family of X : S c= Z } ; :: thesis: {} in Z
then ex S1 being non empty preBoolean Subset-Family of X st
( Z = S1 & S c= S1 ) ;
hence {} in Z by SETFAM_1:def 8; :: thesis: verum

end;

then A2: not Y is empty by A1, SETFAM_1:def 1;

now :: thesis: for A, B being set st A in Y & B in Y holds
A \/ B in Y

let A, B be set ; :: thesis: ( A in Y & B in Y implies A \/ B in Y )
assume B1: ( A in Y & B in Y ) ; :: thesis: A \/ B in Y
for Z being set st Z in { Z where Z is non empty preBoolean Subset-Family of X : S c= Z } holds
A \/ B in Z

proof

let Z be set ; :: thesis: ( Z in { Z where Z is non empty preBoolean Subset-Family of X : S c= Z } implies A \/ B in Z )
assume B2: Z in { Z where Z is non empty preBoolean Subset-Family of X : S c= Z } ; :: thesis: A \/ B in Z
then consider Z1 being non empty preBoolean Subset-Family of X such that
B3: ( Z = Z1 & S c= Z1 ) ;
( A in Z1 & B in Z1 ) by B1, B2, B3, SETFAM_1:def 1;
hence A \/ B in Z by B3, FINSUB_1:def 1; :: thesis: verum

end;

hence A \/ B in Y by A1, SETFAM_1:def 1; :: thesis: verum

end;

then B4: Y is cup-closed ;

now :: thesis: for A, B being set st A in Y & B in Y holds
A \ B in Y

let A, B be set ; :: thesis: ( A in Y & B in Y implies A \ B in Y )
assume C1: ( A in Y & B in Y ) ; :: thesis: A \ B in Y
for Z being set st Z in { Z where Z is non empty preBoolean Subset-Family of X : S c= Z } holds
A \ B in Z

proof

let Z be set ; :: thesis: ( Z in { Z where Z is non empty preBoolean Subset-Family of X : S c= Z } implies A \ B in Z )
assume C2: Z in { Z where Z is non empty preBoolean Subset-Family of X : S c= Z } ; :: thesis: A \ B in Z
then consider Z1 being non empty preBoolean Subset-Family of X such that
C3: ( Z = Z1 & S c= Z1 ) ;
( A in Z1 & B in Z1 ) by C1, C2, C3, SETFAM_1:def 1;
hence A \ B in Z by C3, FINSUB_1:def 3; :: thesis: verum

end;

hence A \ B in Y by A1, SETFAM_1:def 1; :: thesis: verum

end;

then Y is diff-closed ;
hence ex Y being non empty preBoolean Subset-Family of X st Y = meet { Z where Z is non empty preBoolean Subset-Family of X : S c= Z } by A2, B4; :: thesis: verum