hence
ex b1 being set st ( b1indom fi & ( for b2 being set holds ( not b1c= b2 or not b2indom fi or fi . b2=0 ) ) )
; :: thesis: verum
end;
case
1 <>0
; :: thesis: for b1, b2 being set holds ( not b1in 1 or not 1 in b2 or ex b3 being set st ( b3indom fi & ( for b4 being set holds ( not b3c= b4 or not b4indom fi or ( b1in fi . b4 & fi . b4in b2 ) ) ) ) )