let I be set ; :: thesis: for sf being Subset-Family of I
for Z being Subset of I st ( for Z1 being set st Z1 in sf holds
Z c= Z1 ) holds
Z c= Intersect sf
let sf be Subset-Family of I; :: thesis: for Z being Subset of I st ( for Z1 being set st Z1 in sf holds
Z c= Z1 ) holds
Z c= Intersect sf
let Z be Subset of I; :: thesis: ( ( for Z1 being set st Z1 in sf holds
Z c= Z1 ) implies Z c= Intersect sf )
assume A1: for Z1 being set st Z1 in sf holds
Z c= Z1 ; :: thesis: Z c= Intersect sf
per cases ( sf <> {} or sf = {} ) ;
suppose A2: sf <> {} ; :: thesis: Z c= Intersect sf
then Intersect sf = meet sf by SETFAM_1:def 9;
hence Z c= Intersect sf by A1, A2, SETFAM_1:5; :: thesis: verum
end;
suppose sf = {} ; :: thesis: Z c= Intersect sf
then Intersect sf = I by SETFAM_1:def 9;
hence Z c= Intersect sf ; :: thesis: verum
end;
end;